1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Sébastien Gouëzel
5 -/
6
7 import topology.metric_space.hausdorff_distance topology.opens analysis.specific_limits
src └──────────────────────────────────────┘ └────────────┘ └──────────────────────┘
8
9 /-!
10 # Closed subsets
11
12 This file defines the metric and emetric space structure on the types of closed subsets and nonempty compact
13 subsets of a metric or emetric space.
14
15 The Hausdorff distance induces an emetric space structure on the type of closed subsets
16 of an emetric space, called `closeds`. Its completeness, resp. compactness, resp.
17 second-countability, follow from the corresponding properties of the original space.
18
19 In a metric space, the type of nonempty compact subsets (called `nonempty_compacts`) also
20 inherits a metric space structure from the Hausdorff distance, as the Hausdorff edistance is
21 always finite in this context.
22 -/
23
24 noncomputable theory
25 open_locale classical
26 open_locale topological_space
27
28 universe u
29 open classical lattice set function topological_space filter
30
31 namespace emetric
32 section
33 variables {α : Type u} [emetric_space α] {s : set α}
id └───────────┘ └─┘
src └───────────┘ └─┘
typ └───────────┘ └─┘
doc └───────────┘
34
35 /-- In emetric spaces, the Hausdorff edistance defines an emetric space structure
36 on the type of closed subsets -/
37 instance closeds.emetric_space : emetric_space (closeds α) :=
id └───────────┘ └─────┘ ┴
src └───────────┘ └─────┘
typ └───────────┘ └─────┘ ┴
doc └───────────┘ └─────┘
38 { edist := λs t, Hausdorff_edist s.val t.val,
id ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘
src ┴ └─────────────┘ └──┘ └──┘
typ ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘
doc └─────────────┘
39 edist_self := λs, Hausdorff_edist_self,
id ┴ └──────────────────┘
src └──────────────────┘
typ ┴ └──────────────────┘
doc └──────────────────┘
40 edist_comm := λs t, Hausdorff_edist_comm,
id ┴ ┴ └──────────────────┘
src └──────────────────┘
typ ┴ ┴ └──────────────────┘
doc └──────────────────┘
41 edist_triangle := λs t u, Hausdorff_edist_triangle,
id ┴ ┴ ┴ └──────────────────────┘
src └──────────────────────┘
typ ┴ ┴ ┴ └──────────────────────┘
doc └──────────────────────┘
42 eq_of_edist_eq_zero :=
43 λs t h, subtype.eq ((Hausdorff_edist_zero_iff_eq_of_closed s.property t.property).1 h) }
id ┴ ┴ ┴ └────────┘ └───────────────────────────────────┘ ┴└───────┘ ┴└───────┘ ┴ ┴
src └────────┘ └───────────────────────────────────┘ └───────┘ └───────┘ ┴
typ ┴ ┴ ┴ └────────┘ └───────────────────────────────────┘ ┴└───────┘ ┴└───────┘ ┴ ┴
doc └───────────────────────────────────┘
44
45 /-- The edistance to a closed set depends continuously on the point and the set -/
46 lemma continuous_inf_edist_Hausdorff_edist :
47 continuous (λp : α × (closeds α), inf_edist p.1 (p.2).val) :=
id └────────┘ ┴ ┴ └─────┘ ┴ └───────┘ ┴┴ ┴┴ └─┘
src └────────┘ ┴ └─────┘ └───────┘ ┴ ┴ └─┘
typ └────────┘ ┴ ┴ └─────┘ ┴ └───────┘ ┴┴ ┴┴ └─┘
doc └────────┘ └─────┘ └───────┘
48 begin
st └─────
49 refine continuous_of_le_add_edist 2 (by simp) _,
id └────────────────────────┘
src └─────┘└────────────────────────┘└─┘ ┴└──┘└─┘
typ └─────┘└────────────────────────┘└─┘ ┴└──┘└─┘
doc └─────┘ └─┘ ┴└──┘└─┘
txt └─────┘ └─┘ ┴└──┘└─┘
par └─────┘ └─┘ ┴└──┘└─┘
pid ┴ └─┘ └──────┘
st ────────────────────────────────────────┘└───┘└─┘└─
50 rintros ⟨x, s⟩ ⟨y, t⟩,
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
txt └───────────────────┘
par └───────────────────┘
pid └────────────┘
st ──────────────────────┘└─
51 calc inf_edist x (s.val) ≤ inf_edist x (t.val) + Hausdorff_edist (t.val) (s.val) :
id └──┘ └───────┘ ┴ └─────────────┘ └───┘ └───┘
src └──┘ └───────┘ └─────────────┘ └───┘ └───┘
typ └──┘ └───────┘ ┴ └─────────────┘ └───┘ └───┘
doc └──┘ └───────┘ └─────────────┘
st ─────────────────────────────────────────────────────────────────────────────────────
52 inf_edist_le_inf_edist_add_Hausdorff_edist
id └────────────────────────────────────────┘
src └────────────────────────────────────────┘
typ └────────────────────────────────────────┘
doc └────────────────────────────────────────┘
st ───────────────────────────────────────────────
53 ... ≤ (inf_edist y (t.val) + edist x y) + Hausdorff_edist (t.val) (s.val) :
id └───┘ ┴
src └───┘
typ └───┘ ┴
st ──────────────────────────────────────────────────────────────────────────────
54 add_le_add_right' inf_edist_le_inf_edist_add_edist
id └───────────────┘ └──────────────────────────────┘
src └───────────────┘ └──────────────────────────────┘
typ └───────────────┘ └──────────────────────────────┘
doc └──────────────────────────────┘
st ───────────────────────────────────────────────────────
55 ... = inf_edist y (t.val) + (edist x y + Hausdorff_edist (s.val) (t.val)) :
st ──────────────────────────────────────────────────────────────────────────────
56 by simp [add_comm, Hausdorff_edist_comm]
id └──────┘ └──────────────────┘
src └────┘└──────┘└┘└──────────────────┘└─
typ └────┘└──────┘└┘└──────────────────┘└─
doc └────┘ └┘└──────────────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ─────┘└──────────────────────────────────────
57 ... ≤ inf_edist y (t.val) + (edist (x, s) (y, t) + edist (x, s) (y, t)) :
id ┴ ┴
src ─┘ ┴ ┴
typ ─┘ ┴ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─────────────────────────────────────────────────────────────────────────
58 add_le_add_left' (add_le_add' (by simp [edist, le_refl]) (by simp [edist, le_refl]))
id └──────────────┘ └─────────┘ └─────┘ └─────┘
src └──────────────┘ └─────────┘ └────┘ └┘└─────┘┴ └────┘ └┘└─────┘┴
typ └──────────────┘ └─────────┘ └────┘ └┘└─────┘┴ └────┘ └┘└─────┘┴
doc └────┘ └┘ ┴ └────┘ └┘ ┴
txt └────┘ └┘ ┴ └────┘ └┘ ┴
par └────┘ └┘ ┴ └────┘ └┘ ┴
pid ┴┴ └┘ ┴ ┴┴ └┘ ┴
st ────────────────────────────────────┘└────────────────────┘└───┘└────────────────────┘└──
59 ... = inf_edist y (t.val) + 2 * edist (x, s) (y, t) :
id ┴
src ┴
typ ┴
st ────────────────────────────────────────────────────────
60 by rw [← mul_two, mul_comm]
id └─────┘ └──────┘
src └────┘└─────┘└┘└──────┘└┘
typ └────┘└─────┘└┘└──────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid └──┘ └┘ ┴┴
st ─────┘└────────────┘└────────┘┴┴
61 end
st └─┘
62
63 /-- Subsets of a given closed subset form a closed set -/
64 lemma is_closed_subsets_of_is_closed (hs : is_closed s) :
id └───────┘ ┴
src └───────┘
typ └───────┘ ┴
doc └───────┘
65 is_closed {t : closeds α | t.val ⊆ s} :=
id └───────┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
src └───────┘ ┴ └─────┘ └──┘ ┴
typ └───────┘ ┴ └─────┘ ┴ ┴└──┘ ┴ ┴
doc └───────┘ └─────┘
66 begin
st └─────
67 refine is_closed_of_closure_subset (λt ht x hx, _),
id └─────────────────────────┘
src └─────┘└─────────────────────────┘┴ └───────────┘
typ └─────┘└─────────────────────────┘┴ └───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ───────────────────────────────────────────────────┘└─
68 -- t : closeds α, ht : t ∈ closure {t : closeds α | t.val ⊆ s},
st ───────────────────────────────────────────────────────────────────
69 -- x : α, hx : x ∈ t.val
st ────────────────────────────
70 -- goal : x ∈ s
st ──────────────────
71 have : x ∈ closure s,
id ┴ ┴ └─────┘ ┴
src └─────┘ ┴┴┴└─────┘┴
typ └─────┘┴┴┴┴└─────┘┴┴
doc └─────┘ ┴ ┴└─────┘┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴
st ─────────────────────┘└─
72 { refine mem_closure_iff'.2 (λε εpos, _),
id └──────────────┘
src └─────┘└──────────────┘└─┘ └────────┘
typ └─────┘└──────────────┘└─┘ └────────┘
doc └─────┘└──────────────┘└─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ───┘└────────────────────────────────────┘└─
73 rcases mem_closure_iff'.1 ht ε εpos with ⟨u, hu, Dtu⟩,
id └──────────────┘ └┘ ┴ └──┘
src └─────┘└──────────────┘└─┘ ┴ ┴ └────────────────┘
typ └─────┘└──────────────┘└─┘└┘┴┴┴└──┘└────────────────┘
doc └─────┘└──────────────┘└─┘ ┴ ┴ └────────────────┘
txt └─────┘ └─┘ ┴ ┴ └────────────────┘
par └─────┘ └─┘ ┴ ┴ └────────────────┘
pid ┴ └─┘ ┴ ┴ └────────────────┘
st ────────────────────────────────────────────────────────┘└─
74 -- u : closeds α, hu : u ∈ {t : closeds α | t.val ⊆ s}, hu' : edist t u < ε
st ──────────────────────────────────────────────────────────────────────────────────
75 rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dtu with ⟨y, hy, Dxy⟩,
id └───────────────────────────────────┘ └┘ └─┘
src └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
typ └─────┘└───────────────────────────────────┘┴└┘┴└─┘└────────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ────────────────────────────────────────────────────────────────────────┘└─
76 -- y : α, hy : y ∈ u.val, Dxy : edist x y < ε
st ───────────────────────────────────────────────────
77 exact ⟨y, hu hy, Dxy⟩ },
id ┴ └┘ └┘ └─┘
src └────┘ └┘ ┴ └┘ └┘
typ └────┘ ┴└┘└┘┴└┘└┘└─┘└┘
doc └────┘ └┘ ┴ └┘ └┘
txt └────┘ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ └┘
pid ┴ └┘ ┴ └┘ ┴┴
st ─────────────────────────┘└┘└
78 rwa closure_eq_of_is_closed hs at this,
id └─────────────────────┘ └┘
src └──┘└─────────────────────┘┴ └──────┘
typ └──┘└─────────────────────┘┴└┘└──────┘
doc └──┘ ┴ └──────┘
txt └──┘ ┴ └──────┘
par └──┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ───────────────────────────────────────┘└─
79 end
st ──┘
80
81 /-- By definition, the edistance on `closeds α` is given by the Hausdorff edistance -/
82 lemma closeds.edist_eq {s t : closeds α} : edist s t = Hausdorff_edist s.val t.val := rfl
id └─────┘ ┴ └───┘ ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘ └─┘
src └─────┘ └───┘ ┴ └─────────────┘ └──┘ └──┘ └─┘
typ └─────┘ ┴ └───┘ ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘ └─┘
doc └─────┘ └─────────────┘
83
84 /-- In a complete space, the type of closed subsets is complete for the
85 Hausdorff edistance. -/
86 instance closeds.complete_space [complete_space α] : complete_space (closeds α) :=
id └────────────┘ ┴ └────────────┘ └─────┘ ┴
src └────────────┘ └────────────┘ └─────┘
typ └────────────┘ ┴ └────────────┘ └─────┘ ┴
doc └────────────┘ └────────────┘ └─────┘
87 begin
st └─────
88 /- We will show that, if a sequence of sets `s n` satisfies
st ──────────────────────────────────────────────────────────────
89 `edist (s n) (s (n+1)) < 2^{-n}`, then it converges. This is enough to guarantee
st ───────────────────────────────────────────────────────────────────────────────────
90 completeness, by a standard completeness criterion.
st ──────────────────────────────────────────────────────
91 We use the shorthand `B n = 2^{-n}` in ennreal. -/
st ─────────────────────────────────────────────────────
92 let B : ℕ → ennreal := λ n, (2⁻¹)^n,
id └─────┘ └┘ ┴
src └──────┘ ┴ ┴└─────┘└──┘ └──┘ ┴└┘┴┴
typ └──────┘ ┴ ┴└─────┘└──┘ └──┘ ┴└┘┴┴
doc └──────┘ ┴ ┴└─────┘└──┘ └──┘ ┴ ┴
txt └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴
par └──────┘ ┴ ┴ └──┘ └──┘ ┴ ┴
pid └───┘└─┘ ┴ ┴ └──┘ └──┘ ┴ ┴
st ────────────────────────────────────┘└─
93 have B_pos : ∀ n, (0:ennreal) < B n,
id └─────┘ ┴ ┴
src └───────────┘ └┘ ┴ └┘└─────┘└┘┴┴ ┴
typ └───────────┘ └┘ ┴ └┘└─────┘└┘┴┴┴┴
doc └───────────┘ └┘ ┴ └┘└─────┘└┘ ┴ ┴
txt └───────────┘ └┘ ┴ └┘ └┘ ┴ ┴
par └───────────┘ └┘ ┴ └┘ └┘ ┴ ┴
pid └────────┘└─┘ └┘ ┴ └┘ └┘ ┴ ┴
st ────────────────────────────────────┘
94 by simp [B, ennreal.pow_pos],
id ┴ └─────────────┘
src └────┘ └┘└─────────────┘┴
typ └────┘┴└┘└─────────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─
95 have B_ne_top : ∀ n, B n ≠ ⊤,
id ┴ ┴ ┴
src └──────────────┘ └┘ ┴ ┴ ┴┴┴┴
typ └──────────────┘ └┘ ┴┴┴ ┴┴┴┴
doc └──────────────┘ └┘ ┴ ┴ ┴ ┴
txt └──────────────┘ └┘ ┴ ┴ ┴ ┴
par └──────────────┘ └┘ ┴ ┴ ┴ ┴
pid └───────────┘└─┘ └┘ ┴ ┴ ┴ ┴
st ─────────────────────────────┘
96 by simp [B, ennreal.div_def, ennreal.pow_ne_top],
id ┴ └─────────────┘ └────────────────┘
src └────┘ └┘└─────────────┘└┘└────────────────┘┴
typ └────┘┴└┘└─────────────┘└┘└────────────────┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └─
97 /- Consider a sequence of closed sets `s n` with `edist (s n) (s (n+1)) < B n`.
st ──────────────────────────────────────────────────────────────────────────────────
98 We will show that it converges. The limit set is t0 = ⋂n, closure (⋃m≥n, s m).
st ─────────────────────────────────────────────────────────────────────────────────
99 We will have to show that a point in `s n` is close to a point in `t0`, and a point
st ──────────────────────────────────────────────────────────────────────────────────────
100 in `t0` is close to a point in `s n`. The completeness then follows from a
st ─────────────────────────────────────────────────────────────────────────────
101 standard criterion. -/
st ─────────────────────────
102 refine complete_of_convergent_controlled_sequences B B_pos (λs hs, _),
id └─────────────────────────────────────────┘ ┴ └───┘
src └─────┘└─────────────────────────────────────────┘┴ ┴ ┴ └──────┘
typ └─────┘└─────────────────────────────────────────┘┴┴┴└───┘┴ └──────┘
doc └─────┘└─────────────────────────────────────────┘┴ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ ┴ └──────┘
pid ┴ ┴ ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────────────────────┘└─
103 let t0 := ⋂n, closure (⋃m≥n, (s m).val),
id ┴ ┴ └─────┘ ┴ ┴ ┴
src └────────┘┴┴┴┴└─────┘┴ ┴└┘ ┴┴ ┴ └────┘
typ └────────┘┴┴┴┴└─────┘┴ ┴└┘ ┴┴ ┴┴ └────┘
doc └────────┘┴┴┴┴└─────┘┴ ┴└┘ ┴┴ ┴ └────┘
txt └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘
par └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘
pid └────┘┴└─┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘
st ────────────────────────────────────────┘└─
104 let t : closeds α := ⟨t0, is_closed_Inter (λ_, is_closed_closure)⟩,
id └─────┘ ┴ └┘ └─────────────┘ └───────────────┘
src └──────┘└─────┘┴ └──┘ └┘└─────────────┘┴ └─┘└───────────────┘└┘
typ └──────┘└─────┘┴┴└──┘ └┘└┘└─────────────┘┴ └─┘└───────────────┘└┘
doc └──────┘└─────┘┴ └──┘ └┘ ┴ └─┘ └┘
txt └──────┘ ┴ └──┘ └┘ ┴ └─┘ └┘
par └──────┘ ┴ └──┘ └┘ ┴ └─┘ └┘
pid └───┘└─┘ ┴ └──┘ └┘ ┴ └─┘ └┘
st ───────────────────────────────────────────────────────────────────┘└─
105 use t,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ──────┘└─
106 -- The inequality is written this way to agree with `edist_le_of_edist_le_geometric_of_tendsto₀`
st ───────────────────────────────────────────────────────────────────────────────────────────────────
107 have I1 : ∀n:ℕ, ∀x ∈ (s n).val, ∃y ∈ t0, edist x y ≤ 2 * B n,
id ┴ ┴ └┘┴ └───┘ ┴ ┴ ┴
src └────────┘ └┘ ┴ └──┘ ┴ └───┘ ┴┴└──┘ ┴┴└───┘┴ ┴ ┴┴└─┘┴┴ ┴
typ └────────┘ └┘ ┴ └──┘ ┴┴ └───┘ ┴┴└──┘└┘┴┴└───┘┴ ┴ ┴┴└─┘┴┴┴┴
doc └────────┘ └┘ ┴ └──┘ ┴ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
txt └────────┘ └┘ ┴ └──┘ ┴ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
par └────────┘ └┘ ┴ └──┘ ┴ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
pid └─────┘└─┘ └┘ ┴ └──┘ ┴ └───┘ ┴ └──┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
108 { /- This is the main difficulty of the proof. Starting from `x ∈ s n`, we want
st ───┘└─────────────────────────────────────────────────────────────────────────────
109 to find a point in `t0` which is close to `x`. Define inductively a sequence of
st ───────────────────────────────────────────────────────────────────────────────────────
110 points `z m` with `z n = x` and `z m ∈ s m` and `edist (z m) (z (m+1)) ≤ B m`. This is
st ──────────────────────────────────────────────────────────────────────────────────────────────
111 possible since the Hausdorff distance between `s m` and `s (m+1)` is at most `B m`.
st ───────────────────────────────────────────────────────────────────────────────────────────
112 This sequence is a Cauchy sequence, therefore converging as the space is complete, to
st ─────────────────────────────────────────────────────────────────────────────────────────────
113 a limit which satisfies the required properties. -/
st ───────────────────────────────────────────────────────────
114 assume n x hx,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └───────────┘
st ────────────────┘└─
115 obtain ⟨z, hz₀, hz⟩ : ∃ z : Π l, (s (n+l)).val, (z 0:α) = x ∧
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘┴└───┘ └┘ ┴ ┴ ┴ └────┘┴┴ └─┘ └┘┴┴ ┴┴└
typ └────────────────────┘┴└───┘ └┘ ┴ ┴┴ ┴ └────┘┴┴ └─┘ └┘┴┴┴┴┴└
doc └────────────────────┘ └───┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ ┴ ┴ └
txt └────────────────────┘ └───┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ ┴ ┴ └
par └────────────────────┘ └───┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ ┴ ┴ └
pid └──────────────┘ └───┘ └┘ ┴ ┴ └────┘ ┴ └─┘ └┘ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────
116 ∀ k, edist (z k:α) (z (k+1):α) ≤ B n / 2^k,
id └───┘ ┴ ┴ ┴ ┴
src ─────┘ └┘ ┴└───┘┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴┴└┘
typ ─────┘ └┘ ┴└───┘┴ ┴ ┴ └┘ ┴ └─┘┴└┘ ┴┴┴┴┴┴└┘
doc ─────┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
txt ─────┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
par ─────┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
pid ─────┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘
st ───────────────────────────────────────────────┘└─
117 { -- We prove existence of the sequence by induction.
st ─────┘└───────────────────────────────────────────────────
118 have : ∀ (l : ℕ) (z : (s (n+l)).val), ∃ z' : (s (n+l+1)).val, edist (z:α) z' ≤ B n / 2^l,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴
src └─────┘ └────┘ └─────┘ ┴ └─────┘ ┴┴└────┘ ┴ └─────┘┴┴└───┘┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
typ └─────┘ └────┘ └─────┘ ┴ └─────┘ ┴┴└────┘ ┴┴ └─────┘┴┴└───┘┴ ┴┴└┘ ┴ ┴┴┴┴┴ └┘
doc └─────┘ └────┘ └─────┘ ┴ └─────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ └────┘ └─────┘ ┴ └─────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ └────┘ └─────┘ ┴ └─────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ └────┘ └─────┘ ┴ └─────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
119 { assume l z,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────┘└────────┘└─
120 obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ (s (n+l+1)).val, edist (z:α) z' < B n / 2^l,
id ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └─────────────────────────┘┴└────┘ ┴ └─────┘┴┴└───┘┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
typ └─────────────────────────┘┴└────┘ ┴┴ └─────┘┴┴└───┘┴ ┴┴┴└┘ ┴ ┴┴┴┴┴ └┘ ┴
doc └─────────────────────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────────────────────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────────────────────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───────────────────┘ └────┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
121 { apply exists_edist_lt_of_Hausdorff_edist_lt z.2,
id └───────────────────────────────────┘ ┴
src └────┘└───────────────────────────────────┘┴ └┘
typ └────┘└───────────────────────────────────┘┴┴└┘
doc └────┘└───────────────────────────────────┘┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ └┘
st ─────────┘└─────────────────────────────────────────────┘└─
122 simp only [B, ennreal.div_def, ennreal.inv_pow'],
id ┴ └─────────────┘ └──────────────┘
src └─────────┘ └┘└─────────────┘└┘└──────────────┘┴
typ └─────────┘┴└┘└─────────────┘└┘└──────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────┘└─
123 rw [← pow_add],
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ──────────────────────┘└──
124 apply hs; simp },
src └────┘ └───┘
typ └────┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ────────────────────────┘└┘└
125 exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩ },
id └┘ └────┘ └──────┘ └─┘
src └────┘ └┘ └─┘└──────┘┴ └┘
typ └────┘ └┘└┘└────┘└─┘└──────┘┴└─┘└┘
doc └────┘ └┘ └─┘ ┴ └┘
txt └────┘ └┘ └─┘ ┴ └┘
par └────┘ └┘ └─┘ ┴ └┘
pid ┴ └┘ └─┘ ┴ ┴┴
st ──────────────────────────────────────────┘└┘└
126 use [λ k, nat.rec_on k ⟨x, hx⟩ (λl z, some (this l z)), rfl],
id └────────┘ ┴ └┘ └──┘ └──┘ └─┘
src └───┘ └──┘└────────┘┴ ┴ └┘ └┘ └───┘└──┘┴ ┴ ┴ └──┘└─┘┴
typ └───┘ └──┘└────────┘┴ ┴ ┴└┘└┘└┘ └───┘└──┘┴ └──┘┴ ┴ └──┘└─┘┴
doc └───┘ └──┘ ┴ ┴ └┘ └┘ └───┘ ┴ ┴ ┴ └──┘ ┴
txt └───┘ └──┘ ┴ ┴ └┘ └┘ └───┘ ┴ ┴ ┴ └──┘ ┴
par └───┘ └──┘ ┴ ┴ └┘ └┘ └───┘ ┴ ┴ ┴ └──┘ ┴
pid └┘ └──┘ ┴ ┴ └┘ └┘ └───┘ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
127 exact λ k, some_spec (this k _) },
id └───────┘ └──┘
src └────┘ └──┘└───────┘┴ ┴ └──┘
typ └────┘ └──┘└───────┘┴ └──┘┴ └──┘
doc └────┘ └──┘ ┴ ┴ └──┘
txt └────┘ └──┘ ┴ ┴ └──┘
par └────┘ └──┘ ┴ ┴ └──┘
pid ┴ └──┘ ┴ ┴ └─┘┴
st ─────────────────────────────────────┘└┘└
128 -- it follows from the previous bound that `z` is a Cauchy sequence
st ────────────────────────────────────────────────────────────────────────
129 have : cauchy_seq (λ k, ((z k):α)),
id └────────┘ ┴ ┴
src └─────┘└────────┘┴ └──┘ ┴ └┘ └┘
typ └─────┘└────────┘┴ └──┘ ┴┴ └┘┴└┘
doc └─────┘└────────┘┴ └──┘ ┴ └┘ └┘
txt └─────┘ ┴ └──┘ ┴ └┘ └┘
par └─────┘ ┴ └──┘ ┴ └┘ └┘
pid └───┘└┘ ┴ └──┘ ┴ └┘ └┘
st ─────────────────────────────────────┘└─
130 from cauchy_seq_of_edist_le_geometric_two (B n) (B_ne_top n) hz,
id └──────────────────────────────────┘ ┴ └──────┘ ┴ └┘
src └───┘└──────────────────────────────────┘┴ ┴ └┘ ┴ └┘
typ └───┘└──────────────────────────────────┘┴ ┴┴ └┘ └──────┘┴┴└┘└┘
doc └───┘└──────────────────────────────────┘┴ ┴ └┘ ┴ └┘
txt └───┘ ┴ ┴ └┘ ┴ └┘
par └───┘ ┴ ┴ └┘ ┴ └┘
pid └───┘ ┴ ┴ └┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────┘└─
131 -- therefore, it converges
st ───────────────────────────────
132 rcases cauchy_seq_tendsto_of_complete this with ⟨y, y_lim⟩,
id └────────────────────────────┘ └──┘
src └─────┘└────────────────────────────┘┴ └──────────────┘
typ └─────┘└────────────────────────────┘┴└──┘└──────────────┘
doc └─────┘└────────────────────────────┘┴ └──────────────┘
txt └─────┘ ┴ └──────────────┘
par └─────┘ ┴ └──────────────┘
pid ┴ ┴ └──────────────┘
st ─────────────────────────────────────────────────────────────┘└─
133 use y,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ────────┘└─
134 -- the limit point `y` will be the desired point, in `t0` and close to our initial point `x`.
st ──────────────────────────────────────────────────────────────────────────────────────────────────
135 -- First, we check it belongs to `t0`.
st ───────────────────────────────────────────
136 have : y ∈ t0 := mem_Inter.2 (λk, mem_closure_of_tendsto (by simp) y_lim
id ┴ └┘ └───────┘ └────────────────────┘ └───┘
src └─────┘ ┴ ┴ └──┘└───────┘└─┘ └─┘└────────────────────┘┴ ┴└──┘└┘ └
typ └─────┘┴┴ ┴└┘└──┘└───────┘└─┘ └─┘└────────────────────┘┴ ┴└──┘└┘└───┘└
doc └─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ ┴└──┘└┘ └
txt └─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ ┴└──┘└┘ └
par └─────┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ ┴└──┘└┘ └
pid └───┘└┘ ┴ ┴ └──┘ └─┘ └─┘ ┴ └─────┘ └
st ───────────────────────────────────────────────────────────────┘└───┘└───────
137 begin
src ───┘ └
typ ───┘ └
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ───┘└─────
138 simp only [exists_prop, set.mem_Union, filter.mem_at_top_sets, set.mem_preimage, set.preimage_Union],
id └─────────┘ └───────────┘ └────────────────────┘ └──────────────┘ └────────────────┘
src ─────┘└─────────┘└─────────┘└┘└───────────┘└┘└────────────────────┘└┘└──────────────┘└┘└────────────────┘┴└─
typ ─────┘└─────────┘└─────────┘└┘└───────────┘└┘└────────────────────┘└┘└──────────────┘└┘└────────────────┘┴└─
doc ─────┘└─────────┘ └┘ └┘ └┘ └┘ ┴└─
txt ─────┘└─────────┘ └┘ └┘ └┘ └┘ ┴└─
par ─────┘└─────────┘ └┘ └┘ └┘ └┘ ┴└─
pid ────────────────┘ └┘ └┘ └┘ └┘ └──
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
139 exact ⟨k, λ m hm, ⟨n+m, zero_add k ▸ add_le_add (zero_le n) hm, (z m).2⟩⟩
id └──────┘ ┴ ┴ └────────┘ └─────┘ ┴ ┴
src ─────┘└────┘ └┘ └─────┘ └┘└──────┘┴ ┴┴┴└────────┘┴ └─────┘┴ └┘ └┘ ┴ └─────
typ ─────┘└────┘ └┘ └─────┘ └┘└──────┘┴┴┴┴┴└────────┘┴ └─────┘┴┴└┘ └┘ ┴┴ └─────
doc ─────┘└────┘ └┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────
txt ─────┘└────┘ └┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────
par ─────┘└────┘ └┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────
pid ───────────┘ └┘ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └─────
st ────────────────────────────────────────────────────────────────────────────────
140 end),
src ───┘└──┘
typ ───┘└──┘
doc ───┘└──┘
txt ───┘└──┘
par ───┘└──┘
pid ───────┘
st ───┘└─┘┴└─
141 use this,
id └──┘
src └──┘
typ └──┘└──┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st ───────────┘└─
142 -- Then, we check that `y` is close to `x = z n`. This follows from the fact that `y`
st ──────────────────────────────────────────────────────────────────────────────────────────
143 -- is the limit of `z k`, and the distance between `z n` and `z k` has already been estimated.
st ───────────────────────────────────────────────────────────────────────────────────────────────────
144 rw [← hz₀],
id └─┘
src └────┘ ┴
typ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ────────────┘└──
145 exact edist_le_of_edist_le_geometric_two_of_tendsto₀ (B n) hz y_lim },
id └────────────────────────────────────────────┘ ┴ ┴ └┘ └───┘
src └────┘└────────────────────────────────────────────┘┴ ┴ └┘ ┴ ┴
typ └────┘└────────────────────────────────────────────┘┴ ┴┴┴└┘└┘┴└───┘┴
doc └────┘└────────────────────────────────────────────┘┴ ┴ └┘ ┴ ┴
txt └────┘ ┴ ┴ └┘ ┴ ┴
par └────┘ ┴ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└┘└
146 have I2 : ∀n:ℕ, ∀x ∈ t0, ∃y ∈ (s n).val, edist x y ≤ 2 * B n,
id └┘ ┴ ┴ ┴ └───┘ ┴
src └────────┘ └┘ ┴ └──┘ ┴┴└──┘ ┴ └───┘┴┴└───┘┴ ┴ ┴ └─┘ ┴ ┴
typ └────────┘ └┘ ┴ └──┘└┘ ┴┴└──┘ ┴┴ └───┘┴┴└───┘┴ ┴ ┴ └─┘ ┴┴┴
doc └────────┘ └┘ ┴ └──┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
txt └────────┘ └┘ ┴ └──┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
par └────────┘ └┘ ┴ └──┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
pid └─────┘└─┘ └┘ ┴ └──┘ ┴ └──┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────────────┘└─
147 { /- For the (much easier) reverse inequality, we start from a point `x ∈ t0` and we want
st ───┘└───────────────────────────────────────────────────────────────────────────────────────
148 to find a point `y ∈ s n` which is close to `x`.
st ─────────────────────────────────────────────────────────
149 `x` belongs to `t0`, the intersection of the closures. In particular, it is well
st ─────────────────────────────────────────────────────────────────────────────────────────
150 approximated by a point `z` in `⋃m≥n, s m`, say in `s m`. Since `s m` and
st ──────────────────────────────────────────────────────────────────────────────────
151 `s n` are close, this point is itself well approximated by a point `y` in `s n`,
st ─────────────────────────────────────────────────────────────────────────────────────────
152 as required. -/
st ────────────────────────
153 assume n x xt0,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ─────────────────┘└─
154 have : x ∈ closure (⋃m≥n, (s m).val), by apply mem_Inter.1 xt0 n,
id ┴ └─────┘ ┴ ┴┴ ┴ └───────┘ └─┘ ┴
src └─────┘ ┴ ┴└─────┘┴ ┴└┘ ┴┴ ┴ └────┘ └────┘└───────┘└─┘ ┴
typ └─────┘┴┴ ┴└─────┘┴ ┴└┘┴┴┴ ┴┴ └────┘ └────┘└───────┘└─┘└─┘┴┴
doc └─────┘ ┴ ┴└─────┘┴ ┴└┘ ┴┴ ┴ └────┘ └────┘ └─┘ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘ └────┘ └─┘ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘ └────┘ └─┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ └────┘ ┴ └─┘ ┴
st ───────────────────────────────────────┘ └─
155 rcases mem_closure_iff'.1 this (B n) (B_pos n) with ⟨z, hz, Dxz⟩,
id └──────────────┘ └──┘ ┴ └───┘ ┴
src └─────┘└──────────────┘└─┘ ┴ ┴ └┘ ┴ └─────────────────┘
typ └─────┘└──────────────┘└─┘└──┘┴ ┴┴ └┘ └───┘┴┴└─────────────────┘
doc └─────┘└──────────────┘└─┘ ┴ ┴ └┘ ┴ └─────────────────┘
txt └─────┘ └─┘ ┴ ┴ └┘ ┴ └─────────────────┘
par └─────┘ └─┘ ┴ ┴ └┘ ┴ └─────────────────┘
pid ┴ └─┘ ┴ ┴ └┘ ┴ └─────────────────┘
st ───────────────────────────────────────────────────────────────────┘└─
156 -- z : α, Dxz : edist x z < B n,
st ──────────────────────────────────────
157 simp only [exists_prop, set.mem_Union] at hz,
id └─────────┘ └───────────┘
src └─────────┘└─────────┘└┘└───────────┘└─────┘
typ └─────────┘└─────────┘└┘└───────────┘└─────┘
doc └─────────┘ └┘ └─────┘
txt └─────────┘ └┘ └─────┘
par └─────────┘ └┘ └─────┘
pid ┴└──┘└┘ └┘ ┴┴└───┘
st ───────────────────────────────────────────────┘└─
158 rcases hz with ⟨m, ⟨m_ge_n, hm⟩⟩,
id └┘
src └─────┘ └─────────────────────┘
typ └─────┘└┘└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ───────────────────────────────────┘└─
159 -- m : ℕ, m_ge_n : m ≥ n, hm : z ∈ (s m).val
st ─────────────────────────────────────────────────
160 have : Hausdorff_edist (s m).val (s n).val < B n := hs n m n m_ge_n (le_refl n),
id └─────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ └────┘ └─────┘ ┴
src └─────┘└─────────────┘┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─────┘┴ ┴
typ └─────┘└─────────────┘┴ ┴┴└────┘ ┴┴ └────┘ ┴┴┴┴└──┘└┘┴ ┴┴┴ ┴└────┘┴ └─────┘┴┴┴
doc └─────┘└─────────────┘┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ └────┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
161 rcases exists_edist_lt_of_Hausdorff_edist_lt hm this with ⟨y, hy, Dzy⟩,
id └───────────────────────────────────┘ └┘ └──┘
src └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
typ └─────┘└───────────────────────────────────┘┴└┘┴└──┘└────────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
162 -- y : α, hy : y ∈ (s n).val, Dzy : edist z y < B n
st ──────────────────────────────────────────────────────────
163 exact ⟨y, hy, calc
id └┘
src └────┘ └┘ └┘ └
typ └────┘ └┘└┘└┘ └
doc └────┘ └┘ └┘ └
txt └────┘ └┘ └┘ └
par └────┘ └┘ └┘ └
pid ┴ └┘ └┘ └
st ───────────────────────
164 edist x y ≤ edist x z + edist z y : edist_triangle _ _ _
id ┴ └───┘ ┴ ┴ └────────────┘
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ └─┘└────────────┘└──────
typ ─────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└───┘┴┴┴┴└─┘└────────────┘└──────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ───────────────────────────────────────────────────────────────
165 ... ≤ B n + B n : add_le_add' (le_of_lt Dxz) (le_of_lt Dzy)
id └─────────┘ └─┘ └──────┘ └─┘
src ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└─────────┘┴ ┴ └┘ └──────┘┴ └─
typ ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└─────────┘┴ ┴└─┘└┘ └──────┘┴└─┘└─
doc ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └─
txt ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └─
par ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └─
pid ───────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────
166 ... = 2 * B n : (two_mul _).symm ⟩ },
id ┴ ┴ └─────┘
src ───────────────┘ └─┘ ┴ ┴ └─┘ └─────┘└─────────┘
typ ───────────────┘ └─┘ ┴┴┴┴└─┘ └─────┘└─────────┘
doc ───────────────┘ └─┘ ┴ ┴ └─┘ └─────────┘
txt ───────────────┘ └─┘ ┴ ┴ └─┘ └─────────┘
par ───────────────┘ └─┘ ┴ ┴ └─┘ └─────────┘
pid ───────────────┘ └─┘ ┴ ┴ └─┘ └────────┘┴
st ──────────────────────────────────────────────┘└┘└
167 -- Deduce from the above inequalities that the distance between `s n` and `t0` is at most `2 B n`.
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
168 have main : ∀n:ℕ, edist (s n) t ≤ 2 * B n := λn, Hausdorff_edist_le_of_mem_edist (I1 n) (I2 n),
id └───┘ ┴ ┴ ┴ └─────────────────────────────┘ └┘ └┘
src └──────────┘ └┘ ┴└───┘┴ ┴ └┘ ┴ └─┘ ┴ ┴ └──┘ └─┘└─────────────────────────────┘┴ ┴ └┘ ┴ ┴
typ └──────────┘ └┘ ┴└───┘┴ ┴┴ └┘┴┴ └─┘ ┴┴┴ └──┘ └─┘└─────────────────────────────┘┴ └┘┴ └┘ └┘┴ ┴
doc └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └──┘ └─┘└─────────────────────────────┘┴ ┴ └┘ ┴ ┴
txt └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴ ┴
par └──────────┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴ ┴
pid └───────┘└─┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ └──┘ └─┘ ┴ ┴ └┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
169 -- from this, the convergence of `s n` to `t0` follows.
st ──────────────────────────────────────────────────────────
170 refine (tendsto_at_top _).2 (λε εpos, _),
id └────────────┘
src └─────┘ └────────────┘└────┘ └────────┘
typ └─────┘ └────────────┘└────┘ └────────┘
doc └─────┘ └────┘ └────────┘
txt └─────┘ └────┘ └────────┘
par └─────┘ └────┘ └────────┘
pid ┴ └────┘ └────────┘
st ─────────────────────────────────────────┘└─
171 have : tendsto (λn, 2 * B n) at_top (𝓝 (2 * 0)),
id └─────┘ ┴ └────┘ ┴
src └─────┘└─────┘┴ └───┘ ┴ ┴ └┘└────┘┴ ┴┴ └┘ └──┘
typ └─────┘└─────┘┴ └───┘ ┴┴┴ └┘└────┘┴ ┴┴ └┘ └──┘
doc └─────┘└─────┘┴ └───┘ ┴ ┴ └┘└────┘┴ ┴┴ └┘ └──┘
txt └─────┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
par └─────┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
pid └───┘└┘ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘
st ────────────────────────────────────────────────┘└─
172 from ennreal.tendsto.const_mul
id └───────────────────────┘
src └───┘└───────────────────────┘└
typ └───┘└───────────────────────┘└
doc └───┘ └
txt └───┘ └
par └───┘ └
pid └───┘ └
st ───────────────────────────────────
173 (ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 $ by simp [ennreal.one_lt_two])
id └───────────────────────────────────────┘ └────────────────┘
src ─────┘ └───────────────────────────────────────┘┴ ┴ ┴└────┘└────────────────┘┴└─
typ ─────┘ └───────────────────────────────────────┘┴ ┴ ┴└────┘└────────────────┘┴└─
doc ─────┘ ┴ ┴ ┴└────┘ ┴└─
txt ─────┘ ┴ ┴ ┴└────┘ ┴└─
par ─────┘ ┴ ┴ ┴└────┘ ┴└─
pid ─────┘ ┴ ┴ └─────┘ └──
st ────────────────────────────────────────────────────┘└────────────────────────┘└─
174 (or.inr $ by simp),
id └────┘
src ─────┘ └────┘┴ ┴ ┴└──┘┴
typ ─────┘ └────┘┴ ┴ ┴└──┘┴
doc ─────┘ ┴ ┴ ┴└──┘┴
txt ─────┘ ┴ ┴ ┴└──┘┴
par ─────┘ ┴ ┴ ┴└──┘┴
pid ─────┘ ┴ ┴ └────┘
st ─────────────────┘└───┘┴└─
175 rw mul_zero at this,
id └──────┘
src └─┘└──────┘└──────┘
typ └─┘└──────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────────┘└─
176 obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b,
id ┴ ┴ ┴ ┴ ┴
src └───────────────┘┴└┘┴┴ └───┘ ┴ ┴┴└─┘ ┴ ┴
typ └───────────────┘┴└┘┴┴ └───┘ ┴┴┴┴└─┘ ┴┴┴
doc └───────────────┘ └┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴
txt └───────────────┘ └┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴
par └───────────────┘ └┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴
pid └─────────┘ └┘ ┴ └───┘ ┴ ┴ └─┘ ┴ ┴
st ───────────────────────────────────────────┘└─
177 from ((tendsto_order.1 this).2 ε εpos).exists_forall_of_at_top,
id └───────────┘ └──┘ ┴ └──┘
src └───┘ └───────────┘└─┘ └──┘ ┴ └───────────────────────┘
typ └───┘ └───────────┘└─┘└──┘└──┘┴┴└──┘└───────────────────────┘
doc └───┘ └─┘ └──┘ ┴ └───────────────────────┘
txt └───┘ └─┘ └──┘ ┴ └───────────────────────┘
par └───┘ └─┘ └──┘ ┴ └───────────────────────┘
pid └───┘ └─┘ └──┘ ┴ └──────────────────────┘┴
st ─────────────────────────────────────────────────────────────────┘└─
178 exact ⟨N, λn hn, lt_of_le_of_lt (main n) (hN n hn)⟩
id ┴ └────────────┘ └──┘ └┘
src └────┘ └┘ └────┘└────────────┘┴ ┴ └┘ ┴ ┴ └─┘
typ └────┘ ┴└┘ └────┘└────────────┘┴ └──┘┴ └┘ └┘┴ ┴ └─┘
doc └────┘ └┘ └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
txt └────┘ └┘ └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
par └────┘ └┘ └────┘ ┴ ┴ └┘ ┴ ┴ └─┘
pid ┴ └┘ └────┘ ┴ ┴ └┘ ┴ ┴ └┘┴
st ─────────────────────────────────────────────────────┘
179 end
st └─┘
180
181 /-- In a compact space, the type of closed subsets is compact. -/
182 instance closeds.compact_space [compact_space α] : compact_space (closeds α) :=
id └───────────┘ ┴ └───────────┘ └─────┘ ┴
src └───────────┘ └───────────┘ └─────┘
typ └───────────┘ ┴ └───────────┘ └─────┘ ┴
doc └───────────┘ └───────────┘ └─────┘
183 ⟨begin
st └─────
184 /- by completeness, it suffices to show that it is totally bounded,
st ──────────────────────────────────────────────────────────────────────
185 i.e., for all ε>0, there is a finite set which is ε-dense.
st ───────────────────────────────────────────────────────────────
186 start from a set `s` which is ε-dense in α. Then the subsets of `s`
st ────────────────────────────────────────────────────────────────────────
187 are finitely many, and ε-dense for the Hausdorff distance. -/
st ──────────────────────────────────────────────────────────────────
188 refine compact_of_totally_bounded_is_closed (emetric.totally_bounded_iff.2 (λε εpos, _)) is_closed_univ,
id └──────────────────────────────────┘ └─────────────────────────┘ └────────────┘
src └─────┘└──────────────────────────────────┘┴ └─────────────────────────┘└─┘ └──────────┘└────────────┘
typ └─────┘└──────────────────────────────────┘┴ └─────────────────────────┘└─┘ └──────────┘└────────────┘
doc └─────┘ ┴ └─┘ └──────────┘
txt └─────┘ ┴ └─┘ └──────────┘
par └─────┘ ┴ └─┘ └──────────┘
pid ┴ ┴ └─┘ └──────────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
189 rcases dense εpos with ⟨δ, δpos, δlt⟩,
id └───┘ └──┘
src └─────┘└───┘┴ └──────────────────┘
typ └─────┘└───┘┴└──┘└──────────────────┘
doc └─────┘ ┴ └──────────────────┘
txt └─────┘ ┴ └──────────────────┘
par └─────┘ ┴ └──────────────────┘
pid ┴ ┴ └──────────────────┘
st ──────────────────────────────────────┘└─
190 rcases emetric.totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 (@compact_univ α _ _)).1 δ δpos
id └─────────────────────────┘ └──────────────────────────────────┘ └──────────┘ ┴ ┴ └──┘
src └─────┘└─────────────────────────┘└─┘ └──────────────────────────────────┘└─┘ └──────────┘┴ └───────┘ ┴ └
typ └─────┘└─────────────────────────┘└─┘ └──────────────────────────────────┘└─┘ └──────────┘┴┴└───────┘┴┴└──┘└
doc └─────┘ └─┘ └─┘ ┴ └───────┘ ┴ └
txt └─────┘ └─┘ └─┘ ┴ └───────┘ ┴ └
par └─────┘ └─┘ └─┘ ┴ └───────┘ ┴ └
pid ┴ └─┘ └─┘ ┴ └───────┘ ┴ └
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────
191 with ⟨s, fs, hs⟩,
src ───────────────────┘
typ ───────────────────┘
doc ───────────────────┘
txt ───────────────────┘
par ───────────────────┘
pid ───────────────────┘
st ───────────────────┘└─
192 -- s : set α, fs : finite s, hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ
st ──────────────────────────────────────────────────────────────────────────────
193 -- we first show that any set is well approximated by a subset of `s`.
st ─────────────────────────────────────────────────────────────────────────
194 have main : ∀ u : set α, ∃v ⊆ s, Hausdorff_edist u v ≤ δ,
id └─┘ ┴ ┴ ┴┴ └─────────────┘ ┴ ┴
src └──────────┘ └───┘└─┘┴ ┴┴└──┘ ┴┴└─────────────┘┴ ┴ ┴┴┴
typ └──────────┘ └───┘└─┘┴┴ ┴┴└──┘┴┴┴└─────────────┘┴ ┴ ┴┴┴┴
doc └──────────┘ └───┘ ┴ ┴ └──┘ ┴└─────────────┘┴ ┴ ┴ ┴
txt └──────────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
pid └───────┘└─┘ └───┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
195 { assume u,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───┘└──────┘└─
196 let v := {x : α | x ∈ s ∧ ∃y∈u, edist x y < δ},
id ┴ ┴ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
src └───────┘┴└──┘ └─┘ ┴ ┴ ┴ ┴┴└┘ ┴┴└───┘┴ ┴ ┴┴┴ ┴
typ └───────┘┴└──┘┴└─┘ ┴┴┴┴┴ ┴┴└┘┴┴┴└───┘┴ ┴ ┴┴┴┴┴
doc └───────┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └───────┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
par └───────┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ └──┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
197 existsi [v, ((λx hx, hx.1) : v ⊆ s)],
id ┴ ┴ ┴
src └───────┘ └┘ └────┘ └────┘ ┴ ┴ └┘
typ └───────┘┴└┘ └────┘ └────┘┴┴ ┴┴└┘
doc └───────┘ └┘ └────┘ └────┘ ┴ ┴ └┘
txt └───────┘ └┘ └────┘ └────┘ ┴ ┴ └┘
par └───────┘ └┘ └────┘ └────┘ ┴ ┴ └┘
pid └┘ └┘ └────┘ └────┘ ┴ ┴ └┘
st ───────────────────────────────────────┘└─
198 refine Hausdorff_edist_le_of_mem_edist _ _,
id └─────────────────────────────┘
src └─────┘└─────────────────────────────┘└──┘
typ └─────┘└─────────────────────────────┘└──┘
doc └─────┘└─────────────────────────────┘└──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ─────────────────────────────────────────────┘└─
199 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
200 have : x ∈ ⋃y ∈ s, ball y δ := hs (by simp),
id ┴ ┴ ┴┴ └──┘ ┴ └┘
src └─────┘ ┴ ┴┴└──┘ ┴┴└──┘┴ ┴ └──┘ ┴ ┴└──┘┴
typ └─────┘┴┴ ┴┴└──┘┴┴┴└──┘┴ ┴┴└──┘└┘┴ ┴└──┘┴
doc └─────┘ ┴ ┴┴└──┘ ┴┴└──┘┴ ┴ └──┘ ┴ ┴└──┘┴
txt └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘┴
par └─────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴└──┘┴
pid └───┘└┘ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ └────┘
st ──────────────────────────────────────────┘└───┘┴└─
201 rcases mem_bUnion_iff.1 this with ⟨y, ys, dy⟩,
id └────────────┘ └──┘
src └─────┘└────────────┘└─┘ └───────────────┘
typ └─────┘└────────────┘└─┘└──┘└───────────────┘
doc └─────┘ └─┘ └───────────────┘
txt └─────┘ └─┘ └───────────────┘
par └─────┘ └─┘ └───────────────┘
pid ┴ └─┘ └───────────────┘
st ──────────────────────────────────────────────────┘└─
202 have : edist y x < δ := by simp at dy; rwa [edist_comm] at dy,
id └───┘ ┴ ┴ ┴ └────────┘
src └─────┘└───┘┴ ┴ ┴ ┴ └──┘ ┴└────────┘└┘└───┘└────────┘└─────┘
typ └─────┘└───┘┴┴┴┴┴ ┴┴└──┘ ┴└────────┘└┘└───┘└────────┘└─────┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴└────────┘└┘└───┘ └─────┘
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴└────────┘└┘└───┘ └─────┘
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴└────────┘└┘└───┘ └─────┘
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └────────────────┘ └─────┘
st ───────────────────────────────┘└────────────────┘└────────┘┴└────┘└─
203 exact ⟨y, ⟨ys, ⟨x, hx, this⟩⟩, le_of_lt dy⟩ },
id ┴ └┘ ┴ └┘ └──┘ └──────┘ └┘
src └────┘ └┘ └┘ └┘ └┘ └──┘└──────┘┴ └┘
typ └────┘ ┴└┘ └┘└┘ ┴└┘└┘└┘└──┘└──┘└──────┘┴└┘└┘
doc └────┘ └┘ └┘ └┘ └┘ └──┘ ┴ └┘
txt └────┘ └┘ └┘ └┘ └┘ └──┘ ┴ └┘
par └────┘ └┘ └┘ └┘ └┘ └──┘ ┴ └┘
pid ┴ └┘ └┘ └┘ └┘ └──┘ ┴ ┴┴
st ─────────────────────────────────────────────────┘└┘└
204 { rintros x ⟨hx1, ⟨y, yu, hy⟩⟩,
src └──────────────────────────┘
typ └──────────────────────────┘
doc └──────────────────────────┘
txt └──────────────────────────┘
par └──────────────────────────┘
pid └───────────────────┘
st ─────────────────────────────────┘└─
205 exact ⟨y, yu, le_of_lt hy⟩ }},
id ┴ └┘ └──────┘ └┘
src └────┘ └┘ └┘└──────┘┴ └┘
typ └────┘ ┴└┘└┘└┘└──────┘┴└┘└┘
doc └────┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ ┴ └┘
pid ┴ └┘ └┘ ┴ ┴┴
st ────────────────────────────────┘└─┘└
206 -- introduce the set F of all subsets of `s` (seen as members of `closeds α`).
st ─────────────────────────────────────────────────────────────────────────────────
207 let F := {f : closeds α | f.val ⊆ s},
id ┴ └─────┘ ┴ └──┘ ┴
src └───────┘┴└──┘└─────┘┴ └─┘ └──┘┴ ┴ ┴
typ └───────┘┴└──┘└─────┘┴┴└─┘ └──┘┴ ┴┴┴
doc └───────┘ └──┘└─────┘┴ └─┘ ┴ ┴ ┴
txt └───────┘ └──┘ ┴ └─┘ ┴ ┴ ┴
par └───────┘ └──┘ ┴ └─┘ ┴ ┴ ┴
pid └───┘┴└─┘ └──┘ ┴ └─┘ ┴ ┴ ┴
st ─────────────────────────────────────┘└─
208 use F,
id ┴
src └──┘
typ └──┘┴
doc └──┘
txt └──┘
par └──┘
pid ┴
st ──────┘└─
209 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
210 -- `F` is finite
st ───────────────────
211 { apply @finite_of_finite_image _ _ F (λf, f.val),
id └────────────────────┘ ┴
src └────┘ └────────────────────┘└───┘ ┴ └─┘ ┴
typ └────┘ └────────────────────┘└───┘┴┴ └─┘ ┴
doc └────┘ └───┘ ┴ └─┘ ┴
txt └────┘ └───┘ ┴ └─┘ ┴
par └────┘ └───┘ ┴ └─┘ ┴
pid ┴ └───┘ ┴ └─┘ ┴
st ───┘└─────────────────────────────────────────────┘└─
212 { apply set.inj_on_of_injective, simp [subtype.val_injective] },
id └─────────────────────┘ └───────────────────┘
src └────┘└─────────────────────┘ └────┘└───────────────────┘└┘
typ └────┘└─────────────────────┘ └────┘└───────────────────┘└┘
doc └────┘ └────┘ └┘
txt └────┘ └────┘ └┘
par └────┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ─────┘└───────────────────────────┘└─────────────────────────────┘└┘└
213 { refine finite_subset (finite_subsets_of_finite fs) (λb, _),
id └───────────┘ └──────────────────────┘ └┘
src └─────┘└───────────┘┴ └──────────────────────┘┴ └┘ └───┘
typ └─────┘└───────────┘┴ └──────────────────────┘┴└┘└┘ └───┘
doc └─────┘ ┴ └──────────────────────┘┴ └┘ └───┘
txt └─────┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ ┴ └┘ └───┘
st ───────────────────────────────────────────────────────────────┘└─
214 simp only [and_imp, set.mem_image, set.mem_set_of_eq, exists_imp_distrib],
id └─────┘ └───────────┘ └───────────────┘ └────────────────┘
src └─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘┴
typ └─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
215 assume x hx hx',
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ────────────────────┘└─
216 rwa hx' at hx }},
id └─┘
src └──┘ └─────┘
typ └──┘└─┘└─────┘
doc └──┘ └─────┘
txt └──┘ └─────┘
par └──┘ └─────┘
pid ┴ └────┘┴
st ───────────────────┘└─┘└
217 -- `F` is ε-dense
st ────────────────────
218 { assume u _,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ─────────────┘└─
219 rcases main u.val with ⟨t0, t0s, Dut0⟩,
id └──┘ └───┘
src └─────┘ ┴└───┘└───────────────────┘
typ └─────┘└──┘┴└───┘└───────────────────┘
doc └─────┘ ┴ └───────────────────┘
txt └─────┘ ┴ └───────────────────┘
par └─────┘ ┴ └───────────────────┘
pid ┴ ┴ └───────────────────┘
st ─────────────────────────────────────────┘└─
220 have : is_closed t0 := closed_of_compact _ (finite_subset fs t0s).compact,
id └───────┘ └┘ └───────────────┘ └───────────┘ └┘ └─┘
src └─────┘└───────┘┴ └──┘└───────────────┘└─┘ └───────────┘┴ ┴ └───────┘
typ └─────┘└───────┘┴└┘└──┘└───────────────┘└─┘ └───────────┘┴└┘┴└─┘└───────┘
doc └─────┘└───────┘┴ └──┘ └─┘ ┴ ┴ └───────┘
txt └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───────┘
par └─────┘ ┴ └──┘ └─┘ ┴ ┴ └───────┘
pid └───┘└┘ ┴ └──┘ └─┘ ┴ ┴ └──────┘┴
st ────────────────────────────────────────────────────────────────────────────┘└─
221 let t : closeds α := ⟨t0, this⟩,
id └─────┘ ┴ └┘ └──┘
src └──────┘└─────┘┴ └──┘ └┘ ┴
typ └──────┘└─────┘┴┴└──┘ └┘└┘└──┘┴
doc └──────┘└─────┘┴ └──┘ └┘ ┴
txt └──────┘ ┴ └──┘ └┘ ┴
par └──────┘ ┴ └──┘ └┘ ┴
pid └───┘└─┘ ┴ └──┘ └┘ ┴
st ──────────────────────────────────┘└─
222 have : t ∈ F := t0s,
id ┴ ┴ └─┘
src └─────┘ ┴ ┴ └──┘
typ └─────┘┴┴ ┴┴└──┘└─┘
doc └─────┘ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ └──┘
st ──────────────────────┘└─
223 have : edist u t < ε := lt_of_le_of_lt Dut0 δlt,
id └───┘ ┴ ┴ ┴ └────────────┘ └──┘ └─┘
src └─────┘└───┘┴ ┴ ┴ ┴ └──┘└────────────┘┴ ┴
typ └─────┘└───┘┴┴┴┴┴ ┴┴└──┘└────────────┘┴└──┘┴└─┘
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────┘└─
224 apply mem_bUnion_iff.2,
id └────────────┘
src └────┘└────────────┘└┘
typ └────┘└────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────┘└─
225 exact ⟨t, ‹t ∈ F›, this⟩ }
id ┴┴ ┴┴ └──┘
src └────┘ └┘┴ ┴ ┴ ┴└┘ └┘
typ └────┘ └┘┴┴┴ ┴┴┴└┘└──┘└┘
doc └────┘ └┘┴ ┴ ┴ ┴└┘ └┘
txt └────┘ └┘ ┴ ┴ └┘ └┘
par └────┘ └┘ ┴ ┴ └┘ └┘
pid ┴ └┘ ┴ ┴ └┘ ┴┴
st ────────────────────────────┘└─
226 end⟩
st ──┘
227
228 /-- In an emetric space, the type of non-empty compact subsets is an emetric space,
229 where the edistance is the Hausdorff edistance -/
230 instance nonempty_compacts.emetric_space : emetric_space (nonempty_compacts α) :=
id └───────────┘ └───────────────┘ ┴
src └───────────┘ └───────────────┘
typ └───────────┘ └───────────────┘ ┴
doc └───────────┘ └───────────────┘
231 { edist := λs t, Hausdorff_edist s.val t.val,
id ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘
src ┴ └─────────────┘ └──┘ └──┘
typ ┴ ┴ ┴ └─────────────┘ ┴└──┘ ┴└──┘
doc └─────────────┘
232 edist_self := λs, Hausdorff_edist_self,
id ┴ └──────────────────┘
src └──────────────────┘
typ ┴ └──────────────────┘
doc └──────────────────┘
233 edist_comm := λs t, Hausdorff_edist_comm,
id ┴ ┴ └──────────────────┘
src └──────────────────┘
typ ┴ ┴ └──────────────────┘
doc └──────────────────┘
234 edist_triangle := λs t u, Hausdorff_edist_triangle,
id ┴ ┴ ┴ └──────────────────────┘
src └──────────────────────┘
typ ┴ ┴ ┴ └──────────────────────┘
doc └──────────────────────┘
235 eq_of_edist_eq_zero := λs t h, subtype.eq $ begin
id ┴ ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ ┴ └────────┘
st └─────
236 have : closure (s.val) = closure (t.val) := Hausdorff_edist_zero_iff_closure_eq_closure.1 h,
id └───┘ ┴ └─────┘ └───┘ └─────────────────────────────────────────┘ ┴
src └─────┘ ┴ └───┘└┘┴┴└─────┘┴ └───┘└───┘└─────────────────────────────────────────┘└─┘
typ └─────┘ ┴ └───┘└┘┴┴└─────┘┴ └───┘└───┘└─────────────────────────────────────────┘└─┘┴
doc └─────┘ ┴ └┘ ┴└─────┘┴ └───┘└─────────────────────────────────────────┘└─┘
txt └─────┘ ┴ └┘ ┴ ┴ └───┘ └─┘
par └─────┘ ┴ └┘ ┴ ┴ └───┘ └─┘
pid └───┘└┘ ┴ └┘ ┴ ┴ ┴└──┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
237 rwa [closure_eq_iff_is_closed.2 (closed_of_compact _ s.property.2),
id └──────────────────────┘ └───────────────┘ └────────┘
src └───┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└────
typ └───┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└────
doc └───┘ └─┘ └─┘ └────
txt └───┘ └─┘ └─┘ └────
par └───┘ └─┘ └─┘ └────
pid └┘ └─┘ └─┘ └────
st ─────────────────────────────────────────────────────────────────────┘└─
238 closure_eq_iff_is_closed.2 (closed_of_compact _ t.property.2)] at this,
id └──────────────────────┘ └───────────────┘ └────────┘
src ─────────────┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└──────────┘
typ ─────────────┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└──────────┘
doc ─────────────┘ └─┘ └─┘ └──────────┘
txt ─────────────┘ └─┘ └─┘ └──────────┘
par ─────────────┘ └─┘ └─┘ └──────────┘
pid ─────────────┘ └─┘ └─┘ └──┘└──────┘
st ──────────────────────────────────────────────────────────────────────────┘┴└──────┘└─
239 end }
st ────┘
240
241 /-- `nonempty_compacts.to_closeds` is a uniform embedding (as it is an isometry) -/
242 lemma nonempty_compacts.to_closeds.uniform_embedding :
243 uniform_embedding (@nonempty_compacts.to_closeds α _ _) :=
id └───────────────┘ └──────────────────────────┘ ┴
src └───────────────┘ └──────────────────────────┘
typ └───────────────┘ └──────────────────────────┘ ┴
doc └──────────────────────────┘
244 isometry.uniform_embedding $ λx y, rfl
id └────────────────────────┘ ┴ ┴ └─┘
src └────────────────────────┘ └─┘
typ └────────────────────────┘ ┴ ┴ └─┘
doc └────────────────────────┘
245
246 /-- The range of `nonempty_compacts.to_closeds` is closed in a complete space -/
247 lemma nonempty_compacts.is_closed_in_closeds [complete_space α] :
id └────────────┘ ┴
src └────────────┘
typ └────────────┘ ┴
doc └────────────┘
248 is_closed (nonempty_compacts.to_closeds '' (univ : set (nonempty_compacts α))) :=
id └───────┘ └──────────────────────────┘ └┘ └──┘ └─┘ └───────────────┘ ┴
src └───────┘ └──────────────────────────┘ └┘ └──┘ └─┘ └───────────────┘
typ └───────┘ └──────────────────────────┘ └┘ └──┘ └─┘ └───────────────┘ ┴
doc └───────┘ └──────────────────────────┘ └───────────────┘
249 begin
st └─────
250 have : nonempty_compacts.to_closeds '' univ = {s : closeds α | s.val.nonempty ∧ compact s.val},
id └──────────────────────────┘ └┘ └──┘ ┴ ┴ └─────┘ ┴ └──┘└───────┘ ┴ └─────┘
src └─────┘└──────────────────────────┘┴└┘┴└──┘┴┴┴┴└──┘└─────┘┴ └─┘ └──┘└───────┘┴┴┴└─────┘┴ ┴
typ └─────┘└──────────────────────────┘┴└┘┴└──┘┴┴┴┴└──┘└─────┘┴┴└─┘ └──┘└───────┘┴┴┴└─────┘┴ ┴
doc └─────┘└──────────────────────────┘┴ ┴ ┴ ┴ └──┘└─────┘┴ └─┘ └───────┘┴ ┴└─────┘┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
251 { ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ───┘└─┘└─
252 simp only [set.image_univ, set.mem_range, ne.def, set.mem_set_of_eq],
id └────────────┘ └───────────┘ └────┘ └───────────────┘
src └─────────┘└────────────┘└┘└───────────┘└┘└────┘└┘└───────────────┘┴
typ └─────────┘└────────────┘└┘└───────────┘└┘└────┘└┘└───────────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
253 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
254 { rintros ⟨y, hy⟩,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘
st ─────┘└─────────────┘└─
255 have : x.val = y.val := by rcases hy; simp,
id └───┘ └───┘ └┘
src └─────┘└───┘┴ ┴└───┘└──┘ ┴└─────┘ └┘└──┘
typ └─────┘└───┘┴ ┴└───┘└──┘ ┴└─────┘└┘└┘└──┘
doc └─────┘ ┴ ┴ └──┘ ┴└─────┘ └┘└──┘
txt └─────┘ ┴ ┴ └──┘ ┴└─────┘ └┘└──┘
par └─────┘ ┴ ┴ └──┘ ┴└─────┘ └┘└──┘
pid └───┘└┘ ┴ ┴ └──┘ └──────┘ └────┘
st ───────────────────────────────┘└──────────────┘└─
256 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────┘└─
257 exact y.property },
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────┘└┘└
258 { rintros ⟨hx1, hx2⟩,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └─────────┘
st ───────────────────────┘└─
259 existsi (⟨x.val, ⟨hx1, hx2⟩⟩ : nonempty_compacts α),
id └───┘ └─┘ └─┘ └───────────────┘ ┴
src └──────┘ └───┘└┘ └┘ └───┘└───────────────┘┴ ┴
typ └──────┘ └───┘└┘ └─┘└┘└─┘└───┘└───────────────┘┴┴┴
doc └──────┘ └┘ └┘ └───┘└───────────────┘┴ ┴
txt └──────┘ └┘ └┘ └───┘ ┴ ┴
par └──────┘ └┘ └┘ └───┘ ┴ ┴
pid ┴ └┘ └┘ └───┘ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
260 apply subtype.eq,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
261 refl }},
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└─┘└
262 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
263 refine is_closed_of_closure_subset (λs hs, _),
id └─────────────────────────┘
src └─────┘└─────────────────────────┘┴ └──────┘
typ └─────┘└─────────────────────────┘┴ └──────┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ──────────────────────────────────────────────┘└─
264 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
265 { -- take a set set t which is nonempty and at distance at most 1 of s
st ───┘└────────────────────────────────────────────────────────────────────
266 rcases mem_closure_iff'.1 hs 1 ennreal.zero_lt_one with ⟨t, ht, Dst⟩,
id └──────────────┘ └┘ └─────────────────┘
src └─────┘└──────────────┘└─┘ └─┘└─────────────────┘└────────────────┘
typ └─────┘└──────────────┘└─┘└┘└─┘└─────────────────┘└────────────────┘
doc └─────┘└──────────────┘└─┘ └─┘ └────────────────┘
txt └─────┘ └─┘ └─┘ └────────────────┘
par └─────┘ └─┘ └─┘ └────────────────┘
pid ┴ └─┘ └─┘ └────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
267 rw edist_comm at Dst,
id └────────┘
src └─┘└────────┘└─────┘
typ └─┘└────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────┘└─
268 -- this set t contains a point x
st ─────────────────────────────────────
269 rcases ht.1 with ⟨x, hx⟩,
id └┘
src └─────┘ └─────────────┘
typ └─────┘└┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───────────────────────────┘└─
270 -- by the Hausdorff distance control, this point x is at distance at most 1
st ────────────────────────────────────────────────────────────────────────────────
271 -- of a point y in s
st ─────────────────────────
272 rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨y, hy, _⟩,
id └───────────────────────────────────┘ └┘ └─┘
src └─────┘└───────────────────────────────────┘┴ ┴ └──────────────┘
typ └─────┘└───────────────────────────────────┘┴└┘┴└─┘└──────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └──────────────┘
txt └─────┘ ┴ ┴ └──────────────┘
par └─────┘ ┴ ┴ └──────────────┘
pid ┴ ┴ ┴ └──────────────┘
st ──────────────────────────────────────────────────────────────────────┘└─
273 -- this shows that s is not empty
st ──────────────────────────────────────
274 exact ⟨_, hy⟩ },
id └┘
src └────┘ └─┘ └┘
typ └────┘ └─┘└┘└┘
doc └────┘ └─┘ └┘
txt └────┘ └─┘ └┘
par └────┘ └─┘ └┘
pid ┴ └─┘ ┴┴
st ─────────────────┘└┘└
275 { refine compact_iff_totally_bounded_complete.2 ⟨_, is_complete_of_is_closed s.property⟩,
id └──────────────────────────────────┘ └──────────────────────┘ └────────┘
src └─────┘└──────────────────────────────────┘└─┘ └─┘└──────────────────────┘┴└────────┘┴
typ └─────┘└──────────────────────────────────┘└─┘ └─┘└──────────────────────┘┴└────────┘┴
doc └─────┘ └─┘ └─┘ ┴ ┴
txt └─────┘ └─┘ └─┘ ┴ ┴
par └─────┘ └─┘ └─┘ ┴ ┴
pid ┴ └─┘ └─┘ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
276 refine totally_bounded_iff.2 (λε εpos, _),
id └─────────────────┘
src └─────┘└─────────────────┘└─┘ └────────┘
typ └─────┘└─────────────────┘└─┘ └────────┘
doc └─────┘ └─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ────────────────────────────────────────────┘└─
277 -- we have to show that s is covered by finitely many eballs of radius ε
st ─────────────────────────────────────────────────────────────────────────────
278 -- pick a nonempty compact set t at distance at most ε/2 of s
st ──────────────────────────────────────────────────────────────────
279 rcases mem_closure_iff'.1 hs (ε/2) (ennreal.half_pos εpos) with ⟨t, ht, Dst⟩,
id └──────────────┘ └┘ ┴┴ └──────────────┘ └──┘
src └─────┘└──────────────┘└─┘ ┴ ┴└─┘ └──────────────┘┴ └─────────────────┘
typ └─────┘└──────────────┘└─┘└┘┴ ┴┴└─┘ └──────────────┘┴└──┘└─────────────────┘
doc └─────┘└──────────────┘└─┘ ┴ └─┘ ┴ └─────────────────┘
txt └─────┘ └─┘ ┴ └─┘ ┴ └─────────────────┘
par └─────┘ └─┘ ┴ └─┘ ┴ └─────────────────┘
pid ┴ └─┘ ┴ └─┘ ┴ └─────────────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
280 -- cover this space with finitely many balls of radius ε/2
st ───────────────────────────────────────────────────────────────
281 rcases totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 ht.2).1 (ε/2) (ennreal.half_pos εpos)
id └─────────────────┘ └──────────────────────────────────┘ └┘ ┴ └──────────────┘ └──┘
src └─────┘└─────────────────┘└─┘ └──────────────────────────────────┘└─┘ └────┘ └─┘ └──────────────┘┴ └─
typ └─────┘└─────────────────┘└─┘ └──────────────────────────────────┘└─┘└┘└────┘ ┴ └─┘ └──────────────┘┴└──┘└─
doc └─────┘ └─┘ └─┘ └────┘ └─┘ ┴ └─
txt └─────┘ └─┘ └─┘ └────┘ └─┘ ┴ └─
par └─────┘ └─┘ └─┘ └────┘ └─┘ ┴ └─
pid ┴ └─┘ └─┘ └────┘ └─┘ ┴ └─
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────
282 with ⟨u, fu, ut⟩,
src ─────────────────────┘
typ ─────────────────────┘
doc ─────────────────────┘
txt ─────────────────────┘
par ─────────────────────┘
pid ─────────────────────┘
st ─────────────────────┘└─
283 refine ⟨u, ⟨fu, λx hx, _⟩⟩,
id ┴ └┘
src └─────┘ └┘ └┘ └───────┘
typ └─────┘ ┴└┘ └┘└┘ └───────┘
doc └─────┘ └┘ └┘ └───────┘
txt └─────┘ └┘ └┘ └───────┘
par └─────┘ └┘ └┘ └───────┘
pid ┴ └┘ └┘ └───────┘
st ─────────────────────────────┘└─
284 -- u : set α, fu : finite u, ut : t.val ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2)
st ───────────────────────────────────────────────────────────────────────────────────────
285 -- then s is covered by the union of the balls centered at u of radius ε
st ─────────────────────────────────────────────────────────────────────────────
286 rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨z, hz, Dxz⟩,
id └───────────────────────────────────┘ └┘ └─┘
src └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
typ └─────┘└───────────────────────────────────┘┴└┘┴└─┘└────────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ────────────────────────────────────────────────────────────────────────┘└─
287 rcases mem_bUnion_iff.1 (ut hz) with ⟨y, hy, Dzy⟩,
id └────────────┘ └┘ └┘
src └─────┘└────────────┘└─┘ ┴ └─────────────────┘
typ └─────┘└────────────┘└─┘ └┘┴└┘└─────────────────┘
doc └─────┘ └─┘ ┴ └─────────────────┘
txt └─────┘ └─┘ ┴ └─────────────────┘
par └─────┘ └─┘ ┴ └─────────────────┘
pid ┴ └─┘ ┴ └─────────────────┘
st ────────────────────────────────────────────────────┘└─
288 have : edist x y < ε := calc
id └───┘ ┴ ┴ ┴ ┴
src └─────┘└───┘┴ ┴ ┴┴┴ └──┘ └
typ └─────┘└───┘┴┴┴┴┴┴┴┴└──┘ └
doc └─────┘ ┴ ┴ ┴ ┴ └──┘ └
txt └─────┘ ┴ ┴ ┴ ┴ └──┘ └
par └─────┘ ┴ ┴ ┴ ┴ └──┘ └
pid └───┘└┘ ┴ ┴ ┴ ┴ └──┘ └
st ─────────────────────────────────
289 edist x y ≤ edist x z + edist z y : edist_triangle _ _ _
id ┴ └───┘ ┴ ┴ └────────────┘
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ └─┘└────────────┘└──────
typ ─────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└───┘┴┴┴┴└─┘└────────────┘└──────
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ───────────────────────────────────────────────────────────────
290 ... < ε/2 + ε/2 : ennreal.add_lt_add Dxz Dzy
id ┴ └────────────────┘ └─┘ └─┘
src ─────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴ └
typ ─────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴└─┘┴└─┘└
doc ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
txt ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
par ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
pid ─────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └
st ───────────────────────────────────────────────────
291 ... = ε : ennreal.add_halves _,
id ┴ └────────────────┘
src ─────────┘ ┴ └─┘└────────────────┘└┘
typ ─────────┘ ┴┴└─┘└────────────────┘└┘
doc ─────────┘ ┴ └─┘ └┘
txt ─────────┘ ┴ └─┘ └┘
par ─────────┘ ┴ └─┘ └┘
pid ─────────┘ ┴ └─┘ └┘
st ───────────────────────────────────┘└─
292 exact mem_bUnion hy this },
id └────────┘ └┘ └──┘
src └────┘└────────┘┴ ┴ ┴
typ └────┘└────────┘┴└┘┴└──┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────┘└──
293 end
st ──┘
294
295 /-- In a complete space, the type of nonempty compact subsets is complete. This follows
296 from the same statement for closed subsets -/
297 instance nonempty_compacts.complete_space [complete_space α] : complete_space (nonempty_compacts α) :=
id └────────────┘ ┴ └────────────┘ └───────────────┘ ┴
src └────────────┘ └────────────┘ └───────────────┘
typ └────────────┘ ┴ └────────────┘ └───────────────┘ ┴
doc └────────────┘ └────────────┘ └───────────────┘
298 begin
st └─────
299 apply complete_space_of_is_complete_univ,
id └────────────────────────────────┘
src └────┘└────────────────────────────────┘
typ └────┘└────────────────────────────────┘
doc └────┘└────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────────┘└─
300 apply (is_complete_image_iff nonempty_compacts.to_closeds.uniform_embedding).1,
id └───────────────────┘ └────────────────────────────────────────────┘
src └────┘ └───────────────────┘┴└────────────────────────────────────────────┘└─┘
typ └────┘ └───────────────────┘┴└────────────────────────────────────────────┘└─┘
doc └────┘ └───────────────────┘┴└────────────────────────────────────────────┘└─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ ┴└┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
301 apply is_complete_of_is_closed,
id └──────────────────────┘
src └────┘└──────────────────────┘
typ └────┘└──────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────┘└─
302 exact nonempty_compacts.is_closed_in_closeds
id └────────────────────────────────────┘
src └────┘└────────────────────────────────────┘┴
typ └────┘└────────────────────────────────────┘┴
doc └────┘└────────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────────────┘
303 end
st └─┘
304
305 /-- In a compact space, the type of nonempty compact subsets is compact. This follows from
306 the same statement for closed subsets -/
307 instance nonempty_compacts.compact_space [compact_space α] : compact_space (nonempty_compacts α) :=
id └───────────┘ ┴ └───────────┘ └───────────────┘ ┴
src └───────────┘ └───────────┘ └───────────────┘
typ └───────────┘ ┴ └───────────┘ └───────────────┘ ┴
doc └───────────┘ └───────────┘ └───────────────┘
308 ⟨begin
st └─────
309 rw embedding.compact_iff_compact_image nonempty_compacts.to_closeds.uniform_embedding.embedding,
id └─────────────────────────────────┘ └──────────────────────────────────────────────────────┘
src └─┘└─────────────────────────────────┘┴└──────────────────────────────────────────────────────┘
typ └─┘└─────────────────────────────────┘┴└──────────────────────────────────────────────────────┘
doc └─┘ ┴└──────────────────────────────────────────────────────┘
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
310 exact nonempty_compacts.is_closed_in_closeds.compact
id └────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────┘┴
typ └────┘└────────────────────────────────────────────┘┴
doc └────┘└────────────────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────────────────────┘
311 end⟩
st └─┘
312
313 /-- In a second countable space, the type of nonempty compact subsets is second countable -/
314 instance nonempty_compacts.second_countable_topology [second_countable_topology α] :
id └───────────────────────┘ ┴
src └───────────────────────┘
typ └───────────────────────┘ ┴
doc └───────────────────────┘
315 second_countable_topology (nonempty_compacts α) :=
id └───────────────────────┘ └───────────────┘ ┴
src └───────────────────────┘ └───────────────┘
typ └───────────────────────┘ └───────────────┘ ┴
doc └───────────────────────┘ └───────────────┘
316 begin
st └─────
317 haveI : separable_space (nonempty_compacts α) :=
id └─────────────┘ └───────────────┘ ┴
src └──────┘└─────────────┘┴ └───────────────┘┴ └────
typ └──────┘└─────────────┘┴ └───────────────┘┴┴└────
doc └──────┘└─────────────┘┴ └───────────────┘┴ └────
txt └──────┘ ┴ ┴ └────
par └──────┘ ┴ ┴ └────
pid ┴└┘ ┴ ┴ ┴└───
st ───────────────────────────────────────────────────
318 begin
src ─┘ └
typ ─┘ └
doc ─┘ └
txt ─┘ └
par ─┘ └
pid ─┘ └
st ─┘└─────
319 /- To obtain a countable dense subset of `nonempty_compacts α`, start from
src ───────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────
320 a countable dense subset `s` of α, and then consider all its finite nonempty subsets.
src ──────────────────────────────────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────────────────────────────────
321 This set is countable and made of nonempty compact sets. It turns out to be dense:
src ───────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────
322 by total boundedness, any compact set `t` can be covered by finitely many small balls, and
src ───────────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────────
323 approximations in `s` of the centers of these balls give the required finite approximation
src ───────────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────────
324 of `t`. -/
src ───────────────
typ ───────────────
doc ───────────────
txt ───────────────
par ───────────────
pid ───────────────
st ───────────────
325 have : separable_space α := by apply_instance,
id └─────────────┘ ┴
src ───┘└─────┘└─────────────┘┴ └──┘ ┴└────────────┘└─
typ ───┘└─────┘└─────────────┘┴┴└──┘ ┴└────────────┘└─
doc ───┘└─────┘└─────────────┘┴ └──┘ ┴└────────────┘└─
txt ───┘└─────┘ ┴ └──┘ ┴└────────────┘└─
par ───┘└─────┘ ┴ └──┘ ┴└────────────┘└─
pid ──────────┘ ┴ └──┘ └────────────────
st ─────────────────────────────────┘└─────────────┘└─
326 rcases this.exists_countable_closure_eq_univ with ⟨s, cs, s_dense⟩,
id └───────────────────────────────────┘
src ───┘└─────┘└───────────────────────────────────┘└────────────────────┘└─
typ ───┘└─────┘└───────────────────────────────────┘└────────────────────┘└─
doc ───┘└─────┘ └────────────────────┘└─
txt ───┘└─────┘ └────────────────────┘└─
par ───┘└─────┘ └────────────────────┘└─
pid ──────────┘ └───────────────────────
st ─────────────────────────────────────────────────────────────────────┘└─
327 let v0 := {t : set α | finite t ∧ t ⊆ s},
id ┴ └─┘ ┴ └────┘ ┴ ┴
src ───┘└────────┘┴└──┘└─┘┴ └─┘└────┘┴ ┴ ┴ ┴┴┴ ┴└─
typ ───┘└────────┘┴└──┘└─┘┴┴└─┘└────┘┴ ┴ ┴ ┴┴┴┴┴└─
doc ───┘└────────┘ └──┘ ┴ └─┘└────┘┴ ┴ ┴ ┴ ┴ ┴└─
txt ───┘└────────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└─
par ───┘└────────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴└─
pid ─────────────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────┘└─
328 let v : set (nonempty_compacts α) := {t : nonempty_compacts α | t.val ∈ v0},
id └─┘ └───────────────┘ ┴ └───────────────┘ ┴ └──┘ ┴ └┘
src ───┘└──────┘└─┘┴ └───────────────┘┴ └───┘ └──┘└───────────────┘┴ └─┘ └──┘┴┴┴ ┴└─
typ ───┘└──────┘└─┘┴ └───────────────┘┴┴└───┘ └──┘└───────────────┘┴┴└─┘ └──┘┴┴┴└┘┴└─
doc ───┘└──────┘ ┴ └───────────────┘┴ └───┘ └──┘└───────────────┘┴ └─┘ ┴ ┴ ┴└─
txt ───┘└──────┘ ┴ ┴ └───┘ └──┘ ┴ └─┘ ┴ ┴ ┴└─
par ───┘└──────┘ ┴ ┴ └───┘ └──┘ ┴ └─┘ ┴ ┴ ┴└─
pid ───────────┘ ┴ ┴ └───┘ └──┘ ┴ └─┘ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────┘└─
329 refine ⟨⟨v, ⟨_, _⟩⟩⟩,
id ┴
src ───┘└──────┘ └┘ └─────┘└─
typ ───┘└──────┘ ┴└┘ └─────┘└─
doc ───┘└──────┘ └┘ └─────┘└─
txt ───┘└──────┘ └┘ └─────┘└─
par ───┘└──────┘ └┘ └─────┘└─
pid ───────────┘ └┘ └────────
st ────────────────────────┘└─
330 { have : countable (subtype.val '' v),
id └───────┘ └─────────┘ └┘ ┴
src ─────┘└─────┘└───────┘┴ └─────────┘┴└┘┴ ┴└─
typ ─────┘└─────┘└───────┘┴ └─────────┘┴└┘┴┴┴└─
doc ─────┘└─────┘└───────┘┴ ┴ ┴ ┴└─
txt ─────┘└─────┘ ┴ ┴ ┴ ┴└─
par ─────┘└─────┘ ┴ ┴ ┴ ┴└─
pid ────────────┘ ┴ ┴ ┴ └──
st ────┘└──────────────────────────────────┘└─
331 { refine countable_subset (λx hx, _) (countable_set_of_finite_subset cs),
id └──────────────┘ └────────────────────────────┘ └┘
src ───────┘└─────┘└──────────────┘┴ └───────┘ └────────────────────────────┘┴ ┴└─
typ ───────┘└─────┘└──────────────┘┴ └───────┘ └────────────────────────────┘┴└┘┴└─
doc ───────┘└─────┘ ┴ └───────┘ ┴ ┴└─
txt ───────┘└─────┘ ┴ └───────┘ ┴ ┴└─
par ───────┘└─────┘ ┴ └───────┘ ┴ ┴└─
pid ──────────────┘ ┴ └───────┘ ┴ └──
st ──────┘└─────────────────────────────────────────────────────────────────────┘└─
332 rcases (mem_image _ _ _).1 hx with ⟨y, ⟨hy, yx⟩⟩,
id └───────┘ └┘
src ───────┘└─────┘ └───────┘└────────┘ └─────────────────┘└─
typ ───────┘└─────┘ └───────┘└────────┘└┘└─────────────────┘└─
doc ───────┘└─────┘ └────────┘ └─────────────────┘└─
txt ───────┘└─────┘ └────────┘ └─────────────────┘└─
par ───────┘└─────┘ └────────┘ └─────────────────┘└─
pid ──────────────┘ └────────┘ └────────────────────
st ───────────────────────────────────────────────────────┘└─
333 rw ← yx,
id └┘
src ───────┘└───┘ └─
typ ───────┘└───┘└┘└─
doc ───────┘└───┘ └─
txt ───────┘└───┘ └─
par ───────┘└───┘ └─
pid ────────────┘ └─
st ──────────────┘└─
334 exact hy },
id └┘
src ───────┘└────┘ ┴└──
typ ───────┘└────┘└┘┴└──
doc ───────┘└────┘ ┴└──
txt ───────┘└────┘ ┴└──
par ───────┘└────┘ ┴└──
pid ─────────────┘ └───
st ────────────────┘┴└─
335 apply countable_of_injective_of_countable_image _ this,
id └───────────────────────────────────────┘ └──┘
src ─────┘└────┘└───────────────────────────────────────┘└─┘ └─
typ ─────┘└────┘└───────────────────────────────────────┘└─┘└──┘└─
doc ─────┘└────┘ └─┘ └─
txt ─────┘└────┘ └─┘ └─
par ─────┘└────┘ └─┘ └─
pid ───────────┘ └─┘ └─
st ───────────────────────────────────────────────────────────┘└─
336 apply inj_on_of_inj_on_of_subset (injective_iff_inj_on_univ.1 subtype.val_injective)
id └────────────────────────┘ └───────────────────────┘ └───────────────────┘
src ─────┘└────┘└────────────────────────┘┴ └───────────────────────┘└─┘└───────────────────┘└─
typ ─────┘└────┘└────────────────────────┘┴ └───────────────────────┘└─┘└───────────────────┘└─
doc ─────┘└────┘ ┴ └─┘ └─
txt ─────┘└────┘ ┴ └─┘ └─
par ─────┘└────┘ ┴ └─┘ └─
pid ───────────┘ ┴ └─┘ └─
st ───────────────────────────────────────────────────────────────────────────────────────────
337 (subset_univ _) },
id └─────────┘
src ───────┘ └─────────┘└──┘└──
typ ───────┘ └─────────┘└──┘└──
doc ───────┘ └──┘└──
txt ───────┘ └──┘└──
par ───────┘ └──┘└──
pid ───────┘ └──────
st ───────────────────────┘┴└─
338 { refine subset.antisymm (subset_univ _) (λt ht, mem_closure_iff'.2 (λε εpos, _)),
id └─────────────┘ └─────────┘ └──────────────┘
src ─────┘└─────┘└─────────────┘┴ └─────────┘└──┘ └────┘└──────────────┘└─┘ └─────────┘└─
typ ─────┘└─────┘└─────────────┘┴ └─────────┘└──┘ └────┘└──────────────┘└─┘ └─────────┘└─
doc ─────┘└─────┘ ┴ └──┘ └────┘└──────────────┘└─┘ └─────────┘└─
txt ─────┘└─────┘ ┴ └──┘ └────┘ └─┘ └─────────┘└─
par ─────┘└─────┘ ┴ └──┘ └────┘ └─┘ └─────────┘└─
pid ────────────┘ ┴ └──┘ └────┘ └─┘ └────────────
st ────────────────────────────────────────────────────────────────────────────────────┘└─
339 -- t is a compact nonempty set, that we have to approximate uniformly by a a set in `v`.
src ───────────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────────
340 rcases dense εpos with ⟨δ, δpos, δlt⟩,
id └───┘ └──┘
src ─────┘└─────┘└───┘┴ └──────────────────┘└─
typ ─────┘└─────┘└───┘┴└──┘└──────────────────┘└─
doc ─────┘└─────┘ ┴ └──────────────────┘└─
txt ─────┘└─────┘ ┴ └──────────────────┘└─
par ─────┘└─────┘ ┴ └──────────────────┘└─
pid ────────────┘ ┴ └─────────────────────
st ──────────────────────────────────────────┘└─
341 -- construct a map F associating to a point in α an approximating point in s, up to δ/2.
src ───────────────────────────────────────────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────────────────────────────────────────
342 have Exy : ∀x, ∃y, y ∈ s ∧ edist x y < δ/2,
id ┴ ┴ ┴ └───┘ ┴ ┴┴
src ─────┘└─────────┘ ┴ ┴┴┴┴┴ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴┴┴ ┴┴└─
typ ─────┘└─────────┘ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴└───┘┴ ┴ ┴┴┴┴┴┴└─
doc ─────┘└─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
txt ─────┘└─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
par ─────┘└─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
pid ────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────┘└─
343 { assume x,
src ───────┘└──────┘└─
typ ───────┘└──────┘└─
doc ───────┘└──────┘└─
txt ───────┘└──────┘└─
par ───────┘└──────┘└─
pid ──────────────────
st ──────┘└───────┘└─
344 have : x ∈ closure s := by rw s_dense; exact mem_univ _,
id ┴ └─────┘ ┴ └─────┘ └──────┘
src ───────┘└─────┘ ┴ ┴└─────┘┴ └──┘ ┴└─┘ └┘└────┘└──────┘└┘└─
typ ───────┘└─────┘┴┴ ┴└─────┘┴┴└──┘ ┴└─┘└─────┘└┘└────┘└──────┘└┘└─
doc ───────┘└─────┘ ┴ ┴└─────┘┴ └──┘ ┴└─┘ └┘└────┘ └┘└─
txt ───────┘└─────┘ ┴ ┴ ┴ └──┘ ┴└─┘ └┘└────┘ └┘└─
par ───────┘└─────┘ ┴ ┴ ┴ └──┘ ┴└─┘ └┘└────┘ └┘└─
pid ──────────────┘ ┴ ┴ ┴ └──┘ └──┘ └──────┘ └───
st ─────────────────────────────────┘└───────────────────────────┘└─
345 rcases mem_closure_iff'.1 this (δ/2) (ennreal.half_pos δpos) with ⟨y, ys, hy⟩,
id └──────────────┘ └──┘ ┴ └──────────────┘ └──┘
src ───────┘└─────┘└──────────────┘└─┘ ┴ └─┘ └──────────────┘┴ └────────────────┘└─
typ ───────┘└─────┘└──────────────┘└─┘└──┘┴ ┴ └─┘ └──────────────┘┴└──┘└────────────────┘└─
doc ───────┘└─────┘└──────────────┘└─┘ ┴ └─┘ ┴ └────────────────┘└─
txt ───────┘└─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘└─
par ───────┘└─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘└─
pid ──────────────┘ └─┘ ┴ └─┘ ┴ └───────────────────
st ────────────────────────────────────────────────────────────────────────────────────┘└─
346 exact ⟨y, ⟨ys, hy⟩⟩ },
id ┴ └┘ └┘
src ───────┘└────┘ └┘ └┘ └─┘└──
typ ───────┘└────┘ ┴└┘ └┘└┘└┘└─┘└──
doc ───────┘└────┘ └┘ └┘ └─┘└──
txt ───────┘└────┘ └┘ └┘ └─┘└──
par ───────┘└────┘ └┘ └┘ └─┘└──
pid ─────────────┘ └┘ └┘ └─────
st ───────────────────────────┘┴└─
347 let F := λx, some (Exy x),
id └──┘ └─┘
src ─────┘└───────┘ └─┘└──┘┴ ┴ ┴└─
typ ─────┘└───────┘ └─┘└──┘┴ └─┘┴ ┴└─
doc ─────┘└───────┘ └─┘ ┴ ┴ ┴└─
txt ─────┘└───────┘ └─┘ ┴ ┴ ┴└─
par ─────┘└───────┘ └─┘ ┴ ┴ ┴└─
pid ──────────────┘ └─┘ ┴ ┴ └──
st ──────────────────────────────┘└─
348 have Fspec : ∀x, F x ∈ s ∧ edist x (F x) < δ/2 := λx, some_spec (Exy x),
id ┴ └───┘ ┴ ┴ └───────┘ └─┘
src ─────┘└───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴ └┘ ┴ └───┘ └─┘└───────┘┴ ┴ ┴└─
typ ─────┘└───────────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴└───┘┴ ┴ ┴┴ └┘ ┴┴ └───┘ └─┘└───────┘┴ └─┘┴ ┴└─
doc ─────┘└───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ └─┘ ┴ ┴ ┴└─
txt ─────┘└───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ └─┘ ┴ ┴ ┴└─
par ─────┘└───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ └─┘ ┴ ┴ ┴└─
pid ──────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ └─┘ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────────┘└─
349
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
350 -- cover `t` with finitely many balls. Their centers form a set `a`
src ──────────────────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────────────────
351 have : totally_bounded t.val := (compact_iff_totally_bounded_complete.1 t.property.2).1,
id └─────────────┘ └───┘ └──────────────────────────────────┘ └────────┘
src ─────┘└─────┘└─────────────┘┴└───┘└──┘ └──────────────────────────────────┘└─┘└────────┘└───┘└─
typ ─────┘└─────┘└─────────────┘┴└───┘└──┘ └──────────────────────────────────┘└─┘└────────┘└───┘└─
doc ─────┘└─────┘└─────────────┘┴ └──┘ └─┘ └───┘└─
txt ─────┘└─────┘ ┴ └──┘ └─┘ └───┘└─
par ─────┘└─────┘ ┴ └──┘ └─┘ └───┘└─
pid ────────────┘ ┴ └──┘ └─┘ └──────
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
352 rcases totally_bounded_iff.1 this (δ/2) (ennreal.half_pos δpos) with ⟨a, af, ta⟩,
id └─────────────────┘ └──┘ ┴ └──────────────┘ └──┘
src ─────┘└─────┘└─────────────────┘└─┘ ┴ └─┘ └──────────────┘┴ └────────────────┘└─
typ ─────┘└─────┘└─────────────────┘└─┘└──┘┴ ┴ └─┘ └──────────────┘┴└──┘└────────────────┘└─
doc ─────┘└─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘└─
txt ─────┘└─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘└─
par ─────┘└─────┘ └─┘ ┴ └─┘ ┴ └────────────────┘└─
pid ────────────┘ └─┘ ┴ └─┘ ┴ └───────────────────
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
353 -- a : set α, af : finite a, ta : t.val ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2)
src ─────────────────────────────────────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────────────────────────────────────
354 -- replace each center by a nearby approximation in `s`, giving a new set `b`
src ────────────────────────────────────────────────────────────────────────────────────
typ ────────────────────────────────────────────────────────────────────────────────────
doc ────────────────────────────────────────────────────────────────────────────────────
txt ────────────────────────────────────────────────────────────────────────────────────
par ────────────────────────────────────────────────────────────────────────────────────
pid ────────────────────────────────────────────────────────────────────────────────────
st ────────────────────────────────────────────────────────────────────────────────────
355 let b := F '' a,
id ┴ ┴
src ─────┘└───────┘ ┴ ┴ └─
typ ─────┘└───────┘┴┴ ┴┴└─
doc ─────┘└───────┘ ┴ ┴ └─
txt ─────┘└───────┘ ┴ ┴ └─
par ─────┘└───────┘ ┴ ┴ └─
pid ──────────────┘ ┴ ┴ └─
st ────────────────────┘└─
356 have : finite b := finite_image _ af,
id └────┘ ┴ └──────────┘ └┘
src ─────┘└─────┘└────┘┴ └──┘└──────────┘└─┘ └─
typ ─────┘└─────┘└────┘┴┴└──┘└──────────┘└─┘└┘└─
doc ─────┘└─────┘└────┘┴ └──┘ └─┘ └─
txt ─────┘└─────┘ ┴ └──┘ └─┘ └─
par ─────┘└─────┘ ┴ └──┘ └─┘ └─
pid ────────────┘ ┴ └──┘ └─┘ └─
st ─────────────────────────────────────────┘└─
357 have tb : ∀x ∈ t.val, ∃y ∈ b, edist x y < δ,
id └───┘ ┴ ┴┴ └───┘ ┴
src ─────┘└────────┘ └──┘└───┘ ┴┴└──┘ ┴┴└───┘┴ ┴ ┴ ┴ └─
typ ─────┘└────────┘ └──┘└───┘ ┴┴└──┘┴┴┴└───┘┴ ┴ ┴ ┴┴└─
doc ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
txt ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
par ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────┘└─
358 { assume x hx,
src ───────┘└─────────┘└─
typ ───────┘└─────────┘└─
doc ───────┘└─────────┘└─
txt ───────┘└─────────┘└─
par ───────┘└─────────┘└─
pid ─────────────────────
st ──────┘└──────────┘└─
359 rcases mem_bUnion_iff.1 (ta hx) with ⟨z, za, Dxz⟩,
id └────────────┘ └┘ └┘
src ───────┘└─────┘└────────────┘└─┘ ┴ └─────────────────┘└─
typ ───────┘└─────┘└────────────┘└─┘ └┘┴└┘└─────────────────┘└─
doc ───────┘└─────┘ └─┘ ┴ └─────────────────┘└─
txt ───────┘└─────┘ └─┘ ┴ └─────────────────┘└─
par ───────┘└─────┘ └─┘ ┴ └─────────────────┘└─
pid ──────────────┘ └─┘ ┴ └────────────────────
st ────────────────────────────────────────────────────────┘└─
360 existsi [F z, mem_image_of_mem _ za],
id ┴ ┴ └──────────────┘ └┘
src ───────┘└───────┘ ┴ └┘└──────────────┘└─┘ ┴└─
typ ───────┘└───────┘┴┴┴└┘└──────────────┘└─┘└┘┴└─
doc ───────┘└───────┘ ┴ └┘ └─┘ ┴└─
txt ───────┘└───────┘ ┴ └┘ └─┘ ┴└─
par ───────┘└───────┘ ┴ └┘ └─┘ ┴└─
pid ────────────────┘ ┴ └┘ └─┘ └──
st ───────────────────────────────────────────┘└─
361 calc edist x (F z) ≤ edist x z + edist z (F z) : edist_triangle _ _ _
id ┴ └───┘ ┴ └────────────┘
src ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴└───┘┴ ┴ ┴ └──┘└────────────┘└──────
typ ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴┴ ┴ ┴└───┘┴ ┴ ┴┴ └──┘└────────────┘└──────
doc ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
txt ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
par ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
pid ───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └──────
st ──────────────────────────────────────────────────────────────────────────────
362 ... < δ/2 + δ/2 : ennreal.add_lt_add Dxz (Fspec z).2
id ┴ └────────────────┘ └─┘ └───┘ ┴
src ────────────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴ ┴ ┴ └───
typ ────────────────┘ ┴ └┘┴┴ └──┘└────────────────┘┴└─┘┴ └───┘┴┴└───
doc ────────────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └───
txt ────────────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └───
par ────────────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └───
pid ────────────────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────────
363 ... = δ : ennreal.add_halves _ },
id ┴ └────────────────┘
src ────────────────┘ ┴ └─┘└────────────────┘└─────
typ ────────────────┘ ┴┴└─┘└────────────────┘└─────
doc ────────────────┘ ┴ └─┘ └─────
txt ────────────────┘ ┴ └─┘ └─────
par ────────────────┘ ┴ └─┘ └─────
pid ────────────────┘ ┴ └─┘ └─────
st ──────────────────────────────────────────┘└┘└─
364 -- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
src ────────────────────────────────────────────────────────────────────────────────────────────
typ ────────────────────────────────────────────────────────────────────────────────────────────
doc ────────────────────────────────────────────────────────────────────────────────────────────
txt ────────────────────────────────────────────────────────────────────────────────────────────
par ────────────────────────────────────────────────────────────────────────────────────────────
pid ────────────────────────────────────────────────────────────────────────────────────────────
st ────────────────────────────────────────────────────────────────────────────────────────────
365 let c := {y ∈ b | ∃x∈t.val, edist x y < δ},
id ┴ ┴ ┴ └───┘┴ └───┘ ┴
src ─────┘└───────┘┴└──┘ └─┘┴└┘└───┘┴┴└───┘┴ ┴ ┴ ┴ ┴└─
typ ─────┘└───────┘┴└──┘┴└─┘┴└┘└───┘┴┴└───┘┴ ┴ ┴ ┴┴┴└─
doc ─────┘└───────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└─
txt ─────┘└───────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└─
par ─────┘└───────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴└─
pid ──────────────┘ └──┘ └─┘ └┘ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────┘└─
366 have : finite c := finite_subset ‹finite b› (λx hx, hx.1),
id └────┘ ┴ └───────────┘ ┴└────┘ ┴┴
src ─────┘└─────┘└────┘┴ └──┘└───────────┘┴┴└────┘┴ ┴┴ └────┘ └─┘└─
typ ─────┘└─────┘└────┘┴┴└──┘└───────────┘┴┴└────┘┴┴┴┴ └────┘ └─┘└─
doc ─────┘└─────┘└────┘┴ └──┘ ┴┴└────┘┴ ┴┴ └────┘ └─┘└─
txt ─────┘└─────┘ ┴ └──┘ ┴ ┴ ┴ └────┘ └─┘└─
par ─────┘└─────┘ ┴ └──┘ ┴ ┴ ┴ └────┘ └─┘└─
pid ────────────┘ ┴ └──┘ ┴ ┴ ┴ └────┘ └────
st ──────────────────────────────────────────────────────────────┘└─
367 -- points in `t` are well approximated by points in `c`
src ──────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────
368 have tc : ∀x ∈ t.val, ∃y ∈ c, edist x y ≤ δ,
id └───┘ ┴ ┴┴ └───┘ ┴ ┴
src ─────┘└────────┘ └──┘└───┘ ┴┴└──┘ ┴┴└───┘┴ ┴ ┴┴┴ └─
typ ─────┘└────────┘ └──┘└───┘ ┴┴└──┘┴┴┴└───┘┴ ┴ ┴┴┴┴└─
doc ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
txt ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
par ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────┘└─
369 { assume x hx,
src ───────┘└─────────┘└─
typ ───────┘└─────────┘└─
doc ───────┘└─────────┘└─
txt ───────┘└─────────┘└─
par ───────┘└─────────┘└─
pid ─────────────────────
st ──────┘└──────────┘└─
370 rcases tb x hx with ⟨y, yv, Dxy⟩,
id └┘ ┴ └┘
src ───────┘└─────┘ ┴ ┴ └────────────────┘└─
typ ───────┘└─────┘└┘┴┴┴└┘└────────────────┘└─
doc ───────┘└─────┘ ┴ ┴ └────────────────┘└─
txt ───────┘└─────┘ ┴ ┴ └────────────────┘└─
par ───────┘└─────┘ ┴ ┴ └────────────────┘└─
pid ──────────────┘ ┴ ┴ └───────────────────
st ───────────────────────────────────────┘└─
371 have : y ∈ c := by simp [c, -mem_image]; exact ⟨yv, ⟨x, hx, Dxy⟩⟩,
id ┴ ┴ ┴ └┘ ┴ └┘ └─┘
src ───────┘└─────┘ ┴ ┴ └──┘ ┴└────┘ └───────────┘└┘└────┘ └┘ └┘ └┘ └┘└─
typ ───────┘└─────┘┴┴ ┴┴└──┘ ┴└────┘┴└───────────┘└┘└────┘ └┘└┘ ┴└┘└┘└┘└─┘└┘└─
doc ───────┘└─────┘ ┴ ┴ └──┘ ┴└────┘ └───────────┘└┘└────┘ └┘ └┘ └┘ └┘└─
txt ───────┘└─────┘ ┴ ┴ └──┘ ┴└────┘ └───────────┘└┘└────┘ └┘ └┘ └┘ └┘└─
par ───────┘└─────┘ ┴ ┴ └──┘ ┴└────┘ └───────────┘└┘└────┘ └┘ └┘ └┘ └┘└─
pid ──────────────┘ ┴ ┴ └──┘ └─────┘ └───────────────────┘ └┘ └┘ └┘ └───
st ─────────────────────────┘└─────────────────────────────────────────────┘└─
372 exact ⟨y, this, le_of_lt Dxy⟩ },
id ┴ └──┘ └──────┘ └─┘
src ───────┘└────┘ └┘ └┘└──────┘┴ └┘└──
typ ───────┘└────┘ ┴└┘└──┘└┘└──────┘┴└─┘└┘└──
doc ───────┘└────┘ └┘ └┘ ┴ └┘└──
txt ───────┘└────┘ └┘ └┘ ┴ └┘└──
par ───────┘└────┘ └┘ └┘ ┴ └┘└──
pid ─────────────┘ └┘ └┘ ┴ └────
st ─────────────────────────────────────┘┴└─
373 -- points in `c` are well approximated by points in `t`
src ──────────────────────────────────────────────────────────────
typ ──────────────────────────────────────────────────────────────
doc ──────────────────────────────────────────────────────────────
txt ──────────────────────────────────────────────────────────────
par ──────────────────────────────────────────────────────────────
pid ──────────────────────────────────────────────────────────────
st ──────────────────────────────────────────────────────────────
374 have ct : ∀y ∈ c, ∃x ∈ t.val, edist y x ≤ δ,
id ┴ ┴ └───┘┴ └───┘ ┴
src ─────┘└────────┘ └──┘ ┴┴└──┘└───┘┴┴└───┘┴ ┴ ┴ ┴ └─
typ ─────┘└────────┘ └──┘┴ ┴┴└──┘└───┘┴┴└───┘┴ ┴ ┴ ┴┴└─
doc ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
txt ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
par ─────┘└────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────────┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────┘└─
375 { rintros y ⟨hy1, ⟨x, xt, Dyx⟩⟩,
src ───────┘└───────────────────────────┘└─
typ ───────┘└───────────────────────────┘└─
doc ───────┘└───────────────────────────┘└─
txt ───────┘└───────────────────────────┘└─
par ───────┘└───────────────────────────┘└─
pid ───────────────────────────────────────
st ──────┘└────────────────────────────┘└─
376 have : edist y x ≤ δ := calc
id └───┘ ┴ ┴ ┴
src ───────┘└─────┘└───┘┴ ┴ ┴ ┴ └──┘ └
typ ───────┘└─────┘└───┘┴┴┴┴┴ ┴┴└──┘ └
doc ───────┘└─────┘ ┴ ┴ ┴ ┴ └──┘ └
txt ───────┘└─────┘ ┴ ┴ ┴ ┴ └──┘ └
par ───────┘└─────┘ ┴ ┴ ┴ ┴ └──┘ └
pid ──────────────┘ ┴ ┴ ┴ ┴ └──┘ └
st ─────────────────────────────────────
377 edist y x = edist x y : edist_comm _ _
id └───┘ ┴ ┴ └────────┘
src ─────────┘ ┴ ┴ ┴ ┴└───┘┴ ┴ └─┘└────────┘└────
typ ─────────┘ ┴ ┴ ┴ ┴└───┘┴┴┴┴└─┘└────────┘└────
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────
st ─────────────────────────────────────────────────
378 ... ≤ δ : le_of_lt Dyx,
id ┴ └──────┘ └─┘
src ─────────────┘ ┴ └─┘└──────┘┴ └─
typ ─────────────┘ ┴┴└─┘└──────┘┴└─┘└─
doc ─────────────┘ ┴ └─┘ ┴ └─
txt ─────────────┘ ┴ └─┘ ┴ └─
par ─────────────┘ ┴ └─┘ ┴ └─
pid ─────────────┘ ┴ └─┘ ┴ └─
st ───────────────────────────────┘└─
379 exact ⟨x, xt, this⟩ },
id ┴ └┘ └──┘
src ───────┘└────┘ └┘ └┘ └┘└──
typ ───────┘└────┘ ┴└┘└┘└┘└──┘└┘└──
doc ───────┘└────┘ └┘ └┘ └┘└──
txt ───────┘└────┘ └┘ └┘ └┘└──
par ───────┘└────┘ └┘ └┘ └┘└──
pid ─────────────┘ └┘ └┘ └────
st ───────────────────────────┘┴└─
380 -- it follows that their Hausdorff distance is small
src ───────────────────────────────────────────────────────────
typ ───────────────────────────────────────────────────────────
doc ───────────────────────────────────────────────────────────
txt ───────────────────────────────────────────────────────────
par ───────────────────────────────────────────────────────────
pid ───────────────────────────────────────────────────────────
st ───────────────────────────────────────────────────────────
381 have : Hausdorff_edist t.val c ≤ δ :=
id └─────────────┘ └───┘ ┴ ┴
src ─────┘└─────┘└─────────────┘┴└───┘┴ ┴ ┴ └───
typ ─────┘└─────┘└─────────────┘┴└───┘┴┴┴ ┴┴└───
doc ─────┘└─────┘└─────────────┘┴ ┴ ┴ ┴ └───
txt ─────┘└─────┘ ┴ ┴ ┴ ┴ └───
par ─────┘└─────┘ ┴ ┴ ┴ ┴ └───
pid ────────────┘ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────────
382 Hausdorff_edist_le_of_mem_edist tc ct,
id └─────────────────────────────┘ └┘ └┘
src ───────┘└─────────────────────────────┘┴└┘┴ └─
typ ───────┘└─────────────────────────────┘┴└┘┴└┘└─
doc ───────┘└─────────────────────────────┘┴ ┴ └─
txt ───────┘ ┴ ┴ └─
par ───────┘ ┴ ┴ └─
pid ───────┘ ┴ ┴ └─
st ────────────────────────────────────────────┘└─
383 have Dtc : Hausdorff_edist t.val c < ε := lt_of_le_of_lt this δlt,
id └─────────────┘ └───┘ ┴ ┴ └────────────┘ └──┘ └─┘
src ─────┘└─────────┘└─────────────┘┴└───┘┴ ┴ ┴ └──┘└────────────┘┴ ┴ └─
typ ─────┘└─────────┘└─────────────┘┴└───┘┴┴┴ ┴┴└──┘└────────────┘┴└──┘┴└─┘└─
doc ─────┘└─────────┘└─────────────┘┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─
txt ─────┘└─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─
par ─────┘└─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─
pid ────────────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────┘└─
384 -- the set `c` is not empty, as it is well approximated by a nonempty set
src ────────────────────────────────────────────────────────────────────────────────
typ ────────────────────────────────────────────────────────────────────────────────
doc ────────────────────────────────────────────────────────────────────────────────
txt ────────────────────────────────────────────────────────────────────────────────
par ────────────────────────────────────────────────────────────────────────────────
pid ────────────────────────────────────────────────────────────────────────────────
st ────────────────────────────────────────────────────────────────────────────────
385 have hc : c.nonempty,
id └────────┘
src ─────┘└────────┘└────────┘└─
typ ─────┘└────────┘└────────┘└─
doc ─────┘└────────┘└────────┘└─
txt ─────┘└────────┘ └─
par ─────┘└────────┘ └─
pid ───────────────┘ └─
st ─────────────────────────┘└─
386 from nonempty_of_Hausdorff_edist_ne_top t.property.1 (lattice.ne_top_of_lt Dtc),
id └────────────────────────────────┘ └────────┘ └──────────────────┘ └─┘
src ───────┘└───┘└────────────────────────────────┘┴└────────┘└─┘ └──────────────────┘┴ ┴└─
typ ───────┘└───┘└────────────────────────────────┘┴└────────┘└─┘ └──────────────────┘┴└─┘┴└─
doc ───────┘└───┘└────────────────────────────────┘┴ └─┘ ┴ ┴└─
txt ───────┘└───┘ ┴ └─┘ ┴ ┴└─
par ───────┘└───┘ ┴ └─┘ ┴ ┴└─
pid ────────────┘ ┴ └─┘ ┴ └──
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
387 -- let `d` be the version of `c` in the type `nonempty_compacts α`
src ─────────────────────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────────────────────
388 let d : nonempty_compacts α := ⟨c, ⟨hc, ‹finite c›.compact⟩⟩,
id └───────────────┘ ┴ └┘ └────┘ ┴
src ─────┘└──────┘└───────────────┘┴ └──┘ └┘ └┘ └────┘┴ └────────┘└─
typ ─────┘└──────┘└───────────────┘┴┴└──┘ └┘ └┘└┘ └────┘┴┴ └────────┘└─
doc ─────┘└──────┘└───────────────┘┴ └──┘ └┘ └┘ └────┘┴ └────────┘└─
txt ─────┘└──────┘ ┴ └──┘ └┘ └┘ ┴ └────────┘└─
par ─────┘└──────┘ ┴ └──┘ └┘ └┘ ┴ └────────┘└─
pid ─────────────┘ ┴ └──┘ └┘ └┘ ┴ └───────────
st ─────────────────────────────────────────────────────────────────┘└─
389 have : c ⊆ s,
id ┴ ┴
src ─────┘└─────┘ ┴ ┴ └─
typ ─────┘└─────┘┴┴ ┴┴└─
doc ─────┘└─────┘ ┴ ┴ └─
txt ─────┘└─────┘ ┴ ┴ └─
par ─────┘└─────┘ ┴ ┴ └─
pid ────────────┘ ┴ ┴ └─
st ─────────────────┘└─
390 { assume x hx,
src ───────┘└─────────┘└─
typ ───────┘└─────────┘└─
doc ───────┘└─────────┘└─
txt ───────┘└─────────┘└─
par ───────┘└─────────┘└─
pid ─────────────────────
st ──────┘└──────────┘└─
391 rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨ya, yx⟩⟩,
id └───────┘ └┘
src ───────┘└─────┘ └───────┘└────────┘ └───────────────────┘└─
typ ───────┘└─────┘ └───────┘└────────┘└┘└───────────────────┘└─
doc ───────┘└─────┘ └────────┘ └───────────────────┘└─
txt ───────┘└─────┘ └────────┘ └───────────────────┘└─
par ───────┘└─────┘ └────────┘ └───────────────────┘└─
pid ──────────────┘ └────────┘ └──────────────────────
st ─────────────────────────────────────────────────────────┘└─
392 rw ← yx,
id └┘
src ───────┘└───┘ └─
typ ───────┘└───┘└┘└─
doc ───────┘└───┘ └─
txt ───────┘└───┘ └─
par ───────┘└───┘ └─
pid ────────────┘ └─
st ──────────────┘└─
393 exact (Fspec y).1 },
id └───┘ ┴
src ───────┘└────┘ ┴ └──┘└──
typ ───────┘└────┘ └───┘┴┴└──┘└──
doc ───────┘└────┘ ┴ └──┘└──
txt ───────┘└────┘ ┴ └──┘└──
par ───────┘└────┘ ┴ └──┘└──
pid ─────────────┘ ┴ └──────
st ─────────────────────────┘┴└─
394 have : d ∈ v := ⟨‹finite c›, this⟩,
id ┴ ┴ └────┘ ┴ └──┘
src ─────┘└─────┘ ┴ ┴ └──┘ └────┘┴ └┘ ┴└─
typ ─────┘└─────┘┴┴ ┴┴└──┘ └────┘┴┴ └┘└──┘┴└─
doc ─────┘└─────┘ ┴ ┴ └──┘ └────┘┴ └┘ ┴└─
txt ─────┘└─────┘ ┴ ┴ └──┘ ┴ └┘ ┴└─
par ─────┘└─────┘ ┴ ┴ └──┘ ┴ └┘ ┴└─
pid ────────────┘ ┴ ┴ └──┘ ┴ └┘ └──
st ───────────────────────────────────────┘└─
395 -- we have proved that `d` is a good approximation of `t` as requested
src ─────────────────────────────────────────────────────────────────────────────
typ ─────────────────────────────────────────────────────────────────────────────
doc ─────────────────────────────────────────────────────────────────────────────
txt ─────────────────────────────────────────────────────────────────────────────
par ─────────────────────────────────────────────────────────────────────────────
pid ─────────────────────────────────────────────────────────────────────────────
st ─────────────────────────────────────────────────────────────────────────────
396 exact ⟨d, ‹d ∈ v›, Dtc⟩ },
id ┴ ┴ └─┘
src ─────┘└────┘ └┘ ┴ ┴ └┘ └┘└──
typ ─────┘└────┘ └┘ ┴┴ ┴┴ └┘└─┘└┘└──
doc ─────┘└────┘ └┘ ┴ ┴ └┘ └┘└──
txt ─────┘└────┘ └┘ ┴ ┴ └┘ └┘└──
par ─────┘└────┘ └┘ ┴ ┴ └┘ └┘└──
pid ───────────┘ └┘ ┴ ┴ └┘ └────
st ─────────────────────────────┘└──
397 end,
src ────┘
typ ────┘
doc ────┘
txt ────┘
par ────┘
pid ────┘
st ────┘└─
398 apply second_countable_of_separable,
id └───────────────────────────┘
src └────┘└───────────────────────────┘
typ └────┘└───────────────────────────┘
doc └────┘└───────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────────┘└─
399 end
st ──┘
400
401 end --section
402 end emetric --namespace
403
404 namespace metric
405 section
406
407 variables {α : Type u} [metric_space α]
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
408
409 /-- `nonempty_compacts α` inherits a metric space structure, as the Hausdorff
410 edistance between two such sets is finite. -/
411 instance nonempty_compacts.metric_space : metric_space (nonempty_compacts α) :=
id └──────────┘ └───────────────┘ ┴
src └──────────┘ └───────────────┘
typ └──────────┘ └───────────────┘ ┴
doc └──────────┘ └───────────────┘
412 emetric_space.to_metric_space $ λx y, Hausdorff_edist_ne_top_of_nonempty_of_bounded x.2.1 y.2.1
id └───────────────────────────┘ ┴ ┴ └───────────────────────────────────────────┘ ┴┴ ┴ ┴┴ ┴
src └───────────────────────────┘ └───────────────────────────────────────────┘ ┴ ┴ ┴ ┴
typ └───────────────────────────┘ ┴ ┴ └───────────────────────────────────────────┘ ┴┴ ┴ ┴┴ ┴
doc └───────────────────────────┘ └───────────────────────────────────────────┘
413 (bounded_of_compact x.2.2) (bounded_of_compact y.2.2)
id └────────────────┘ ┴┴ ┴ └────────────────┘ ┴┴ ┴
src └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴
typ └────────────────┘ ┴┴ ┴ └────────────────┘ ┴┴ ┴
doc └────────────────┘ └────────────────┘
414
415 /-- The distance on `nonempty_compacts α` is the Hausdorff distance, by construction -/
416 lemma nonempty_compacts.dist_eq {x y : nonempty_compacts α} :
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
417 dist x y = Hausdorff_dist x.val y.val := rfl
id └──┘ ┴ ┴ ┴ └────────────┘ ┴└──┘ ┴└──┘ └─┘
src └──┘ ┴ └────────────┘ └──┘ └──┘ └─┘
typ └──┘ ┴ ┴ ┴ └────────────┘ ┴└──┘ ┴└──┘ └─┘
doc └────────────┘
418
419 lemma lipschitz_inf_dist_set (x : α) :
id ┴
typ ┴
420 lipschitz_with 1 (λ s : nonempty_compacts α, inf_dist x s.val) :=
id └────────────┘ └───────────────┘ ┴ └──────┘ ┴ ┴└──┘
src └────────────┘ └───────────────┘ └──────┘ └──┘
typ └────────────┘ └───────────────┘ ┴ └──────┘ ┴ ┴└──┘
doc └────────────┘ └───────────────┘ └──────┘
421 lipschitz_with.one_of_le_add $ assume s t,
id └──────────────────────────┘ ┴ ┴
src └──────────────────────────┘
typ └──────────────────────────┘ ┴ ┴
422 by { rw dist_comm,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └─────────────┘└─
423 exact inf_dist_le_inf_dist_add_Hausdorff_dist (edist_ne_top t s) }
id └─────────────────────────────────────┘ └──────────┘ ┴ ┴
src └────┘└─────────────────────────────────────┘┴ └──────────┘┴ ┴ └┘
typ └────┘└─────────────────────────────────────┘┴ └──────────┘┴┴┴┴└┘
doc └────┘└─────────────────────────────────────┘┴ └──────────┘┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────┘└┘
424
425 lemma lipschitz_inf_dist :
426 lipschitz_with 2 (λ p : α × (nonempty_compacts α), inf_dist p.1 p.2.val) :=
id └────────────┘ ┴ ┴ └───────────────┘ ┴ └──────┘ ┴┴ ┴┴ └─┘
src └────────────┘ ┴ └───────────────┘ └──────┘ ┴ ┴ └─┘
typ └────────────┘ ┴ ┴ └───────────────┘ ┴ └──────┘ ┴┴ ┴┴ └─┘
doc └────────────┘ └───────────────┘ └──────┘
427 @lipschitz_with.uncurry' _ _ _ _ _ _ (λ (x : α) (s : nonempty_compacts α), inf_dist x s.val) 1 1
id └─────────────────────┘ ┴ └───────────────┘ ┴ └──────┘ ┴ ┴└──┘
src └─────────────────────┘ └───────────────┘ └──────┘ └──┘
typ └─────────────────────┘ ┴ └───────────────┘ ┴ └──────┘ ┴ ┴└──┘
doc └───────────────┘ └──────┘
428 (λ s, lipschitz_inf_dist_pt s.val) lipschitz_inf_dist_set
id ┴ └───────────────────┘ ┴└──┘ └────────────────────┘
src └───────────────────┘ └──┘ └────────────────────┘
typ ┴ └───────────────────┘ ┴└──┘ └────────────────────┘
doc └───────────────────┘
429
430 lemma uniform_continuous_inf_dist_Hausdorff_dist :
431 uniform_continuous (λp : α × (nonempty_compacts α), inf_dist p.1 (p.2).val) :=
id └────────────────┘ ┴ ┴ └───────────────┘ ┴ └──────┘ ┴┴ ┴┴ └─┘
src └────────────────┘ ┴ └───────────────┘ └──────┘ ┴ ┴ └─┘
typ └────────────────┘ ┴ ┴ └───────────────┘ ┴ └──────┘ ┴┴ ┴┴ └─┘
doc └───────────────┘ └──────┘
432 lipschitz_inf_dist.to_uniform_continuous
id └────────────────┘└────────────────────┘
src └────────────────┘└────────────────────┘
typ └────────────────┘└────────────────────┘
doc └────────────────────┘
433
434 end --section
435 end metric --namespace